Applying the B Method


The B Method is a method of software development based on the B language. Based on an abstract machine notation and industry-strenght tool, it is used in the development of computer software. The B Method allows:

  • to write specification models and to verify their correctness by proof

  • to write (intermediate or final) refinements, to verify their correctness and their compliancy with their specification

  • to check that final refinements, also called implementations, comply with implementability rules (also called B0 compliancy - B0 being the subset of B used only for implementation)

  • to generate source code (C for Atelier B Community version, Ada for the Maintenance version) from implementation models.

Atelier B is the tool implementing the B Method. It has been qualified with the release of the parisian automatic metro line 14 in 1998. Version 4.7 is going to be certified in 2022.

Atelier B comes with a number of tools and features enabling an industrial use for certified applications, both for software development (mainly railway industry - EN50158 certification) and for system modeling (microelectronics - Common Criteria certification).

The B Development Cycle

The B Method is composed of 3 main phases:

  • the project management and the modeling

  • the proof of the models

  • the code generation

A B project is considered correct only when all proof obligations have been proved.

Proof and code generation are independent. Source code could be generated even if a B project is not demonstrated at 100%. Of course, such a source code comes with no garanty at all.

The proof is related to the B models, not to:

  • the natural language requirements: traceability and coverage between requirements and B models have to be checked by humans

  • the source code generated: code generator is not formally developed and proved - so other means are required to ensure a safe execution like software (and possibly hardware) diversity with the use of two different code generators and a runtime verification of their execution with a voter (2 out of 2 architecture).

Last updated