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.
