Links

Applying the B Method

Introduction

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
The B method is composed of number of steps - each step is actionable as a Atelier B command.
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).