Banca de QUALIFICAÇÃO: VALERIO GUTEMBERG DE MEDEIROS JUNIOR

Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.
DISCENTE: VALERIO GUTEMBERG DE MEDEIROS JUNIOR
DATA: 27/02/2015
HORA: 09:00
LOCAL: Sala de reuniões do DIMAp
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: 100
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
RESUMO:
A síntese de código de montagem é um processo que exige rigoroso cuidado. Normalmente, esse processo nos tradutores e compiladores mais maduros é relativamente seguro, apesar 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 verificação usando o método B são apresentadas. Uma primeira abordagem propõe a tradução do componente B para 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 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 melhor aproveita as técnicas de verificação e a aperfeiçoa sua interface. A fim de viabilizar uma tradução mais eficiente e também segura, uma segunda proposta de tradução B para código de máquina virtual foi desenvolvida. Essa técnica de tradução utiliza 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. Tal tradutor também suporta a avaliação de cobertura de código e a inserção de anotações de rastreabilidade. Dessa forma, o trabalho proposto pretende desenvolver significativamente a tradução B para código de montagem e oferecer suporte rigoroso para verificação da tradução. 

MEMBROS DA BANCA:
Presidente - 2220777 - DAVID BORIS PAUL DEHARBE
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Externo à Instituição - ALEXANDRE CABRAL MOTA - UFPE
Externo à Instituição - BRUNO EMERSON GURGEL GOMES - IFRN
Notícia cadastrada em: 20/01/2015 10:39
SIGAA | Superintendência de Informática - (84) 3215-3148 | Copyright © 2006-2017 - UFRN - sigaa09-producao.info.ufrn.br.sigaa09-producao