Banca de DEFESA: VALERIO GUTEMBERG DE MEDEIROS JUNIOR

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
DISCENTE: VALERIO GUTEMBERG DE MEDEIROS JUNIOR
DATA: 08/03/2016
HORA: 09:00
LOCAL: VC03 - SINFO
TÍTULO:

Método B e a síntese verificada para código de montagem


PALAVRAS-CHAVES:

Métodos Formais. Método B. Tradução de Modelos. Verificação de Tradução. Linguagem de Montagem. 


PÁGINAS: 138
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
ESPECIALIDADE: Engenharia de Software
RESUMO:

A síntese de código de montagem é um processo que exige um cuidado rigoroso. Normalmente, esse processo nos tradutores e nos compiladores mais maduros é relativamente seguro, apesar de que, esporadicamente, erros são identificados neles. Em um contexto mais restrito, os tradutores utilizados em comunidades menores e em constante desenvolvimento são mais suscetíveis a erros. Considerando esse contexto, duas abordagens de tradução e de verificação usando o método B são apresentadas. A primeira abordagem propõe a tradução do componente B para o código de montagem de uma plataforma específica, usando um modelo formal do conjunto de instruções, o qual possibilita também depurar e verificar as propriedades de programas. Essa abordagem é capaz de garantir formalmente a coerência semântica da tradução, apesar de ser um processo de verificação árduo e lento. Tal esforço de verificação foi aliviado através de uma ferramenta desenvolvida (BEval), que aproveitou melhor as técnicas de verificação. Após o processo de prova automática usando uma ferramenta B robusta (Atelier B), BEval ainda foi capaz de resolver em certos modelos muitas das obrigações de prova remanescentes, chegando a até 88% do total de obrigações. Contudo, o processo de verificação da abordagem de tradução continuou complexo, exigindo várias interações manuais. Afim de viabilizar uma tradução mais eficiente e também segura, uma segunda abordagem de tradução de B para o código de máquina virtual foi desenvolvida. A segunda abordagem utilizou o tradutor desenvolvido B2LLVM e aplicou a geração automática de testes para verificar a coerência entre a especificação do programa e o seu respectivo código de montagem. Esse tradutor também suporta a avaliação de cobertura do código e a inserção de anotações de rastreabilidade. Dessa forma, o trabalho contribuiu significativamente na tradução de B para o código de montagem, oferecendo um suporte rigoroso para a verificação da tradução. Atualmente, o B2LLVM já é capaz de gerar código para 84% dos exemplos de teste baseados na gramática que são traduzíveis por um relevante tradutor industrial (C4B). Ademais, o código gerado por B2LLVM apresenta vantagens importantes na ampla capacidade de verificação, de integração e de otimização. 


MEMBROS DA BANCA:
Presidente - 1221251 - MARTIN ALEJANDRO MUSICANTE
Interno - 2220777 - DAVID BORIS PAUL DEHARBE
Interno - 1639701 - MARCEL VINÍCIUS MEDEIROS OLIVEIRA
Externo à Instituição - ALEXANDRE CABRAL MOTA - UFPE
Externo à Instituição - BRUNO EMERSON GURGEL GOMES - IFRN
Notícia cadastrada em: 03/03/2016 14:51
SIGAA | Superintendência de Informática - (84) 3215-3148 | Copyright © 2006-2017 - UFRN - sigaa09-producao.info.ufrn.br.sigaa09-producao