masterThesis
Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B
Fecha
2015-03-09Registro en:
FRAGOSO, Paulo Ewerton Gomes. Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B. 2015. 70f. Dissertação (Mestrado em Sistemas e Computação) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2015.
Autor
Fragoso, Paulo Ewerton Gomes
Resumen
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.