Banca de QUALIFICAÇÃO: PAULO EWERTON GOMES FRAGOSO

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE: PAULO EWERTON GOMES FRAGOSO
DATA: 08/10/2014
HORA: 10:30
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: 58
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
Notícia cadastrada em: 26/09/2014 09:34
SIGAA | Superintendência de Tecnologia da Informação - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa11-producao.info.ufrn.br.sigaa11-producao