Event B

Dominique Méry 1, 2 Neeraj Kumar Singh 3
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : Event B is a modelling language which can describe state-based models and required safety properties. The main objective is to provide a technique for incremental and proof-based development of the reactive systems. It integrates set-theoretical notations and a first-order predicate calculus, models called machines; it includes the concept of refinement expressing the simulation of machine by another one. An Event B machine models a reactive system i.e. a system driven by its environment and to its stimuli. An important property of these machines is that its events preserve the invariant properties defining a set of reachable states. The Evenet B method has been developed from the classical B method and it offers a general framework for developing the correct by construction systems by using an incremental approach for designing the models by refinement. Refinement is a relationship relating two models such that one model is simulating the other one. Refinement is also called refinement and preserves properties of the abstract model in the refined or concrete model. When an abstract model is refined by a concrete model, it means that the concrete model simulates the abstract model and that any safety property of the abstract model is also a safety property of the concrete model. In particular, the concrete model preserves the invariant properties of the abstract model. Event B aims to express models of systems characterized by its invariant and by a list of safety properties. However, we can consider liveness properties as in UNITY or TLA+ but in a restricted way.
Complete list of metadatas

https://hal.inria.fr/hal-00926335
Contributor : Dominique Méry <>
Submitted on : Thursday, January 9, 2014 - 2:35:45 PM
Last modification on : Thursday, September 19, 2019 - 1:14:02 AM

Identifiers

  • HAL Id : hal-00926335, version 1

Collections

Citation

Dominique Méry, Neeraj Kumar Singh. Event B. Jean-Louis Boulanger. Mise en oeuvre de la méthode B, HERMES, 2013, Informatique et Systèmes d'Informations, ISBN : 978-2-7462-3810-7. ⟨hal-00926335⟩

Share

Metrics

Record views

509