Formal Design with B Master 1, 2011–2012

B Method

The B method is a design process to develop software, starting from abstract specifications of the software's behavior, and iteratively refining the specifications until they become directly implementable. Refinement guarantees that the resulting implementation conforms to the initial abstract specification. The B method is used for the development of industrial critical systems (for instance, safety-critical software parts of the driver-less metro line 14 in Paris).

Abstract specifications and refinements are written in a formal language with a precise, unambiguous semantics: the B language. Correctness of a B development is expressed by proof obligations, which can be automatically generated. These obligations, once proved with the help of a theorem prover, guarantee:

  1. The coherency of the initial abstract specification, and
  2. The downward compatibility of each refinement.

Several tools are available to support the B method. Some of these tools are capable of translating into code (C, C++, Ada, …) specifications that are sufficiently detailed.

The course introduces the main notions of the B method (abstract machines, refinements, generalized substitutions, proof obligations, composition primitives), and provides an initiation to Atelier B, which fully supports the B-method, including translation into code.

Lab Sessions

The course includes hands-on lab sessions to put the B method into practice. Developments are realized with Atelier B v4.0, the free version of Atelier B. Atelier B comes with both a GUI (graphical user interface) and a CLI (command-line interface). Run the command startAB to start the GUI, or startBB to start the CLI.

In addition to Atelier B, the ProB animator and model-checker is used to simulate B specifications. Refer to the ProB tutorial and user manual for more information.

Atelier B Documentation

Manuals are included in the local Atelier B installation, and they are directly accessible from the GUI. The tool's web site also provides extensive documentation, including manuals and examples. Here are some direct links:

Atelier B Library

A library of reusable components was provided with Atelier B v3.x (commercial releases), and available as a pre-defined project named LIBRARY. This library is not included with Atelier B v4.0. However, an archive may be downloaded from the ComenC page of ClearSy's Open Wiki. This archive contains a C translation of the BASIC_IO machine, which provides vt100-style input/output. The C translation is compatible with the C translator of Atelier B v4.0. Here are some direct links to the library's archive and its documentation:

Handouts and Solutions

Some lab sessions come with written instructions, and some don't. When available, handouts will be posted here. The same applies for solutions.

References

Bibliography

Links

Extra

Documentation

The manuals provided with Atelier B are extensive, which may seem overwhelming at first. To overcome this difficulty, some home-grown succint documentation is provided below. This material is derived from the various sources of documentation mentioned above.

Project and Exam

Example Developments