Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B - Fragoso, Paulo Ewerton Gomes (2015)
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.