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

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

PreviousTraining Slides NextProject Creation

Last updated 2 years ago

Introduction

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.

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