The industrial tool to efficiently deploy the B method

WHAT IS
B METHOD?

B is a formal specification method which, thanks to an adequate language, allows for highly accurate expressions of the properties required by specifications.

MOOC Massive Open Oline Course

+ 20 hours de vidéos

This course introduces the B-method : the basic concepts ranging from the most basic structures like the B machine to proofs using the Atelier-B interactive prover.

MOOC Massive Open Oline Course

B & Event-B models

A collection of Formal Specifications (University of Dusseldorf). With this shared repository, B models from different origins are available for education and self-improvement.

WHY USE
ATELIER B?

The ATELIER B is a tool for the operational use of the FORMAL METHOD B.
It offers, within a coherent environment, numerous functionalities allowing to manage projects in B language.

MOOC Massive Open Oline Course

Basic & Advanced
training

Introduction videos

With these videos, you are going to be introduced to the tool and learn how to use it practically, for both software development and system modelling.

Logo Atelier B

Training resources

Articles & B models

Collection of formal models and articles. These resources allow improving self skills in modeling, proof, and code generation.

ATELIER B,
PRESENTATION

Developed by CLEARSY, Atelier B is an industrial tool that allows for the operational use of the B Method to develop defect-free proven software (formal software). 

It is available in 2 versions:
1- Community Edition available to anyone without any restriction,
2- Maintenance Edition for maintenance contract holders only.

It is used to develop safety automatisms for the various subways installed throughout the world by Alstom and Siemens, and also for Common Criteria certification and the development of system models by integrated device manufacturers.

Additionally, it has been used in a number of other sectors, such as the automotive industry, to model operational principles for the onboard electronics of three car models. Atelier B is also used in the aeronautics and aerospace sectors.

B METHOD,
FOR RELIABLE SOFTWARE

B is a formal specification method which, thanks to an adequate language, allows for highly accurate expressions of the properties required by specifications. One can then prove in a fully automated fashionthat these properties are unambiguous, coherent and are not contradictory. This then allows us to mathematically prove that these properties are taken into account as the design stages progress.