The Event-B Modelling Method - Concepts and Case Studies

Dominique Cansell 1 Dominique Méry 1, *
* Auteur correspondant
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 developingB 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 Event 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. Case studies are illustrating the Event B method.
Type de document :
Chapitre d'ouvrage
Dines Bjoerner and Martin Henson. Logics of Specification Languages, Springer, pp.33-140, 2008, Monographs in Theoretical Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00579550
Contributeur : Dominique Méry <>
Soumis le : jeudi 24 mars 2011 - 11:16:00
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Identifiants

  • HAL Id : inria-00579550, version 1

Collections

Citation

Dominique Cansell, Dominique Méry. The Event-B Modelling Method - Concepts and Case Studies. Dines Bjoerner and Martin Henson. Logics of Specification Languages, Springer, pp.33-140, 2008, Monographs in Theoretical Computer Science. 〈inria-00579550〉

Partager

Métriques

Consultations de la notice

147