Modeling Systems and Proving their Correctness with Event-B and Rodin





Publicado en

Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018)

Licencia Creative Commons


Event-B is a formal development method. It can be used to model and verify correctness of sequential, concurrent, and reactive systems. It uses (infinite) discrete transition systems to capture how the model evolves and first-order logic and typed set theory to express the desirable properties of the system. The proofs that these properties hold are performed using sequent calculus. There are deduction rules specific for useful theories. Event-B is however is not restricted to classical set-theoretical notations and the sequent calculus: it includes notations for defining transitions over states of the model which resembles a programming language, and a rich mathematical toolkit (including operations and relations on sets and functions) to build complex models easily.


Acerca de Carro, Manuel

Palabras clave

Correctness By Construction, Formal Proofs, Rigorous Software Development
Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX