HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Tutorial on the event-based B method : Concepts and Case Studies

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00100065
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 10:13:49 AM
Last modification on : Friday, February 4, 2022 - 3:30:04 AM

Identifiers

  • HAL Id : inria-00100065, version 1

Collections

Citation

Dominique Cansell, Dominique Méry. Tutorial on the event-based B method : Concepts and Case Studies. Logics of Formal Software Specification Languages - LFSL'2004, 2004, The High Tatras, Slovakia. ⟨inria-00100065⟩

Share

Metrics

Record views

123