Banca de DEFESA: PAULO EWERTON GOMES FRAGOSO

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE: PAULO EWERTON GOMES FRAGOSO
DATA: 09/03/2015
HORA: 09:00
LOCAL: Sala de reuniões do DIMAp
TÍTULO:

Contribuições para o Processo de Verificação de Satisfatibilidade Módulo Teoria em Event-B.


PALAVRAS-CHAVES:

Event-B, Solucionadores SMT, Plataforma Rodin, Obrigações de prova, Verificação formal. 


PÁGINAS: 70
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:

Event-B é um método formal de modelagem e verificação de sistemas de transição discre- tos. O desenvolvimento com Event-B produz obrigações de prova que devem ser verifica- das, isto é, ter sua validade verificada para manter a consistência dos modelos produzidos, bem como certificá-los em relação aos requisitos do sistema modelado. Solucionadores de Satisfatibilidade Módulo Teoria são provadores automáticos de teoremas usados para ve- rificar a satisfatibilidade de fórmulas lógicas considerando uma teoria (ou combinação de teorias) subjacente. Solucionadores SMT não apenas lidam com fórmulas extensas em lógica de primeira ordem, como também podem gerar modelos e provas, bem como identi- ficar núcleo insatisfatível. O suporte ferramental para Event-B é provido pela Plataforma Rodin: um IDE extensível, baseado no framework Eclipse, que combina funcionalidades de modelagem e prova. Um plug-in SMT para Rodin tem sido desenvolvido com o objetivo de integrar à plataforma técnicas alternativas e eficientes de verificação. Este trabalho propõe uma série de complementos ao plug-in para solucionadores SMT em Rodin, a sa- ber, melhorias de usabilidade que podem impactar positivamente a produtividade quando obrigações de prova são reportadas como inválidas (isto é, satisfatíveis ou desconhecidas) pelo plug-in. Adicionalmente, algumas modificações na forma como o plug-in lida com resultados válidos por exemplo, ao manipular provas e núcleos insatisfatíveis para gerar novas regras de prova são também consideradas. 


MEMBROS DA BANCA:
Presidente - 2220777 - DAVID BORIS PAUL DEHARBE
Interno - 1639701 - MARCEL VINÍCIUS MEDEIROS OLIVEIRA
Externo ao Programa - 2042860 - RICHARD WALTER ALAIN BONICHON
Externo à Instituição - BRUNO EMERSON GURGEL GOMES - IFRN
Notícia cadastrada em: 11/02/2015 16:30
SIGAA | Superintendência de Informática - (84) 3215-3148 | Copyright © 2006-2017 - UFRN - sigaa03-producao.info.ufrn.br.sigaa03-producao