Tutorial : The B formal method

M. Ducassé
IRISA/INSA
Campus Universitaire de Beaulieu
F-35042 Rennes Cedex
ducasse@irisa.fr
 http://www.irisa.fr/lande/ducasse/

The B formal method has recently been successfully used by Matra Transport and the RATP to specify and implement the critical parts of the new Meteor underground in Paris. Over 100 000 lines of B have been written from which over 80 000 lines of ADA have been automatically generated ; 30 000 proofs had to be done, of which 92% could be automatically discharged by the "Atelier-B" tool. No unit tests were performed. The software worked straightforwardly during the on-site tests and the dead-lines were kept.

B has been designed by J.-R. Abrial. It is the successor of the Z specification formalism and is rooted in the seminal works of Floyd and Hoare. The theoretical background is rather simple, basically first order logic with sets and relations. Experiences with software engineering students show that casual programmers have no problem to master the method.

The key paradigm is the "abstract machine", close to the notion of object without inheritance. Abstract machines are specified, then refined step by step until implementation. At each stage proof obligations are generated in order to insure that invariant properties are preserved.  When all the "local" proofs have been performed, the method guarantees that the software "globally" preserves all the invariants.

The tutorial will list the theoretical notions grounding the B method. It will then present the generalized substitutions which are the basic tools to express, in an elegant way, non executable specifications. It will then briefly describe the refinement and implementation processes. Proof obligation formulas will be discussed. All notions will be illustrated throughout a simple case study.
 

See http://www.atelierb.societe.com