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 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).