Skip to Main content Skip to Navigation
Lectures

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 metadatas

Cited literature [83 references]  Display  Hide  Download

https://cel.archives-ouvertes.fr/inria-00092846
Contributor : Dominique Méry <>
Submitted on : Wednesday, September 13, 2006 - 10:11:21 AM
Last modification on : Thursday, September 19, 2019 - 1:14:01 AM
Long-term archiving on: : Thursday, September 20, 2012 - 10:25:56 AM

Identifiers

  • HAL Id : inria-00092846, version 1

Collections

Citation

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

Share

Metrics

Record views

1026

Files downloads

6859