Búsqueda avanzada

Modeling Systems and Proving their Correctness with Event-B and Rodin (Tutorial)


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.

Palabras Clave:

Correctness by Construction - Formal proofs - Rigorous software development





Este artículo tiene una licencia de uso CreativeCommons - Reconocimiento (by)

Descarga el artículo haciendo click aquí.

Ver la referencia en formato Bibtex