Atelier B

Atelier B is a tool enabling the operational use of B method. In a coherent environment, it provides many functions for managing projects in B language.

For industrial use, it is available in 2 versions:

• The Atelier B Professional Edition is regularly updated and includes exclusive features such as an Ada translator, a Project Checker, and tools for proving mathematical rules. It can be used in industrial settings requiring close support, as well as in academic environments. It is available on request via a maintenance contract.
• The Atelier B T2 Certified Edition, with its T2 certification, enables the development of critical software compliant with EN 50128 and the validation of system properties compliant with EN 50129 for SIL4 applications. A replay tool, Certifier, guarantees that projects developed with a recent Atelier B comply with standards. It is available on request for industrial applications, and offers the same exclusive features as the Atelier B Professional Edition.

Functions

These functions can be divided into four categories:

• proof aid, to demonstrate proof obligations using suitable proof tools
• Development aid: automatic management of dependency between B components,
• User comfort tools: graphical representation of projects, display of project status and statistics, project archiving.

Use of Atelier B

Atelier B is either used via a Man Machine Interface in QT format or using the commands directly (command mode). Atelier B is multi-user. Tasks that can be automated during project development are the following:

• Syntax verification of components
• Automatic proof obligation generation
• Automatic translation of B installations to C or Ada language

Currently, Atelier B is available in Windows, Linux, Mac OS and Solaris operating systems.

ATELIER B and website

visit the web site: www.atelierb.eu