26th IFIP WG 6.1 International Conference on Formal Methods for Networked and Distributed Systems
Special focus on verified middleware and distributed services

Tutorial on the event B method

B is a method for specifying, designing and coding software systems and was designed by J.-R. Abrial. It is based on Zermelo-Fraenkel set theory with the axiom of choice, the concept of generalized substitution and on structuring mechanisms (machine,refinement, implementation). The concept of refinement is the key notion for developing B models of (software) systems in an incremental way. B models are accompanied by mathematical proofs that justify them. Proofs of B models convince the user (designer or specifier) that the (software) system is effectively correct. The presentation will focus on the event B method and we will introduce detail the underlying logic of the B method and the semantic concepts related to the B method; we will detail the B development process partially supported by the mechanical engine of the prover.
The event~B method reuses the set-theoretical and logical notations of the B method and provides new notations for expressing abstract systems or simply models based on events. Moreover, the refinement over models is a key feature for incrementally developing models from a textually-defined system, while preserving correctness; it implements the proof-based development paradigm. Each development. includes proofs for invariance and refinement.Events modify the system state (or state variables, by executing an action, but if a guard holds: an event is not called but observed. When refining machines in classic B, one should maintain the number of operations both in the abstract machine and in the refinement; on the contrary, new events may be introduced in the refinement model and they may modify only new variables. New events bring new proof obligations for ensuring a correct refinement. Finally, an event B model is a closed system with a finite list of state variables and a finite list of events. If the system reacts to its environment, the event~~B model should integrate events of the environment.
The presentation will be based on case studies to illustrate the applicability of the event B method and how to use the tool, namely Click'n'Prove developed by J.-R. Abrial and D. Cansell.