Navegando por Autor "Fragoso, Paulo Ewerton Gomes"
Agora exibindo 1 - 1 de 1
- Resultados por página
- Opções de Ordenação
Dissertação Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B(Universidade Federal do Rio Grande do Norte, 2015-03-09) Fragoso, Paulo Ewerton Gomes; Deharbe, David Boris Paul; ; http://lattes.cnpq.br/2985658685449858; ; http://lattes.cnpq.br/9393335275523504; Gomes, Bruno Emerson Gurgel; ; http://lattes.cnpq.br/7812661521592212; Oliveira, Marcel Vinícius Medeiros; ; http://lattes.cnpq.br/1756952696097255; Bonichon, Richard Walter Alain;Event-B é um método formal de modelagem e verificação de sistemas de transição discretos. O desenvolvimento com Event-B produz obrigações de prova que devem ser verificadas, isto é, ter sua validade verificada para manter a consistência dos modelos produzidos. Solucionadores de Satisfatibilidade Módulo Teoria são provadores automáticos de teoremas usados para verificar 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 identificar subconjuntos insatisfatíveis de hipóteses (núcleos insatisfatíveis). 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. Neste trabalho foi implementada uma série de complementos ao plug-in para solucionadores SMT em Rodin, a saber, melhorias na interface do usuário para quando obrigações de prova são reportadas como inválidas pelo plug-in. Adicionalmente, algumas características do plug-in, tais como suporte à geração de provas e extração de núcleo insatisfatível, foram modificadas de modo a tornaremse compatíveis com o padrão SMT-LIB para solucionadores SMT. Realizaram-se testes utilizando obrigações de prova aplicáveis para demonstrar as novas funcionalidades. As contribuições descritas podem, potencialmente, afetar a produtividade de forma positiva.