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