Training

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

The “B formal method” traditionally refers to the set comprising :
the B language, the refinement, the proof and the associated tools.

ATELIER B

FEATURES

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

ATELIER B

It can be used either through a Human Machine Interface in Qt or by using commands directly (batch mode). The tasks that can be automated during the development of a project are the following:
– Syntax checks of components
– Automatic generation of proof obligations
– Automatic translation of B implementations to C or Ada languages.

Atelier B is available for Windows, Linux, Mac OS and Solaris.

Visit atelier B website

The B Method

Event-driven B is a specialisation of the formal B method, which is used to formally describe systems and reason mathematically about their properties.

The B method is a formal specification method which allows, thanks to an adequate language, to express very rigorously the properties required by a specification. It is then possible to prove automatically that these properties are unambiguous, coherent and not contradictory.