PRESENTATION
Why use Atelier B?
Functionalities
– Availability of Atelier B in Linux, Mac OS X and Windows, thanks to the development of the graphic interface in the Qt environment and the transfer of the Atelier B core tools.
– A replay tool, the Certifier, certified T2, guarantees that projects developed with a recent Atelier B comply with EN50128 and 50129standards.
– A graphical interface that offers, in particular:
- An all-in-one overview of the projects and their status, a better integration of error messages.
- An editor with browsing and automatic completion that supports the B Language and Event-B.
- The inclusion of a task distributor: the development tasks (type verification, generation of proof obligations, automatic proof, code generation) can be distributed among a pool of servers. The interface allows for the adding, deleting and interrupting of these tasks.
- A reworked proof interface with better management of the proof tree, simplified access to proof commands, the addition of user rules and the syntactic analysis of formulas.
– Event-B support with syntactic controls and the generation of specific proof obligations.
– A translator from B0 implementation to the C language (ComenC).
– A translator from B0 implementation to the Rust language (B2rust).
– Proof of the well-definedness: automatic, integrated creation of a well-definedness project associated with a main project to validate the well-definedness.
– An automatic refinement tool (BART).