Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.

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.