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.
+ 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.
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.
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.
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
Atelier B is the industrial tool that enables the B formal method to be used operationally for the development of software that has been proven flawless (formal software), or for validating the safety properties of a system.
It is available in 4 versions:
1- Atelier B Community Edition
2- Atelier B Professional Edition
3- Atelier B T2 Certified Edition
4- Atelier B CSP Educational Version
The Atelier B Community Edition is a fully functional version of Atelier B, updated every 2 years. It can be downloaded free of charge from this site, and is free to use.
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.
The Atelier B CSP Educational Version is a special version of the Atelier B Community Edition, which lets you program a safety controller (the CLEARSY Safety Platform) integrated into a demonstration circuit board. It provides an introduction to the programming of critical control applications.
Atelier B is used in particular for the development of safety-related automatic control systems for the various metros developed worldwide by Alstom, Siemens, etc., for certification to the “Common Criteria” standard and the development of microcircuits by the semiconductor industry, and to guarantee system safety.
It is also used in other sectors, such as the automotive industry, to model the operating principles of on-board electronics on 3 car models.
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.