Skip to Main content Skip to Navigation

Tutorial on the event-based B method

Dominique Cansell 1 Dominique Méry 1 
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : B is a method for specifying, designing and coding software systems. 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. We provide a survey of the underlying logic of the B method and the semantic concepts related to the B method; we detail the B development process partially supported by the mechanical engine of the prover.
Complete list of metadata

Cited literature [83 references]  Display  Hide  Download
Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Wednesday, September 13, 2006 - 10:11:21 AM
Last modification on : Friday, February 4, 2022 - 3:34:11 AM
Long-term archiving on: : Thursday, September 20, 2012 - 10:25:56 AM


  • HAL Id : inria-00092846, version 1



Dominique Cansell, Dominique Méry. Tutorial on the event-based B method. IFIP FORTE 2006 Paris, 2006. ⟨inria-00092846⟩



Record views


Files downloads