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.
Liste complète des métadonnées

Littérature citée [83 références]  Voir  Masquer  Télécharger

Contributeur : Dominique Méry <>
Soumis le : mercredi 13 septembre 2006 - 10:11:21
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : jeudi 20 septembre 2012 - 10:25:56


  • 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〉



Consultations de la notice


Téléchargements de fichiers