Home -
News -
Products -
Versions -
Download -
Manuals
- Maintenance -
Distribution Policy -
Roadmap & Contribution -
Support -
Training -
Documents -
Press -
References -
R&D - Contacts -
Jobs -
Links -
Your Account
The B Compiler
Presentation
With the Theorem Generator and the Theorem Demonstrator, the B compiler is one of Atelier B’s main tools.
It allows for an analysis of the syntax of B models and the verification of the coherence of types, as well as the rules on
the construction and visibility of models in a B project. It therefore is a powerful library that
allows for new applications to be created.
For example:
| Tools | Presentation |
BART |
An automatic refinement tool. This tool lets you automate the installation of abstract B machines by applying the refinement rules. Siemens Transportation Systems uses a similar tool to develop automatic pilots for subways. |
|---|---|
B2Ladder |
A translator that produces a Ladder (a contact language used by programmable automatons in industry) graphic model based on a B model. This translator is specific to the Siemens S7 automaton family. |
Btags |
A tool that generates navigation information for the Atelier B v4.0, Emacs and vi model editor. It accepts the entry into B machines of the mathematical rules used for proof with Atelier B, as well as BART refinement rules. |
B2Rodin |
Transformation of an event B model (in Atelier B text format) into a Rodin xml model. |
The Cross-referencer (CrossRef) |
A tool to generate dictionaries of terms. |
Translators of B to C, ADA and High Integrity ADA (industrial) |
|