Several tools (developed, under development or planned to be developed) are discussed in these pages.
- C4B : currently the default C code generator delivered with Atelier B 4 (community and maintenance versions). This code generator, based on the B-Compiler, is developped in C++/Qt.
- Tradada : (High Integrity) Ada code generator that comes with the Atelier B 4 maintenance version only.
- ComenC : previous C code generator, based on obsolete libraries. Not supported / distributed anymore.
- B2Ladder : Ladder code generator, used internally by ClearSy for railways safety critical applications. This code generator, based on the B-Compiler, is developped in C++/Qt.
- B2List : Instruction list code generator, used internally by ClearSy for railways safety critical applications. This code generator, based on the B-Compiler, is developped in C++/Qt.
- B4SYN : VHDL code generator, jointly developped with STMicroelectronics. Distribution would start in 2014.
Other code generators (Assembly language, C for microcontrolers, LLVM, binary files, etc.) are currently under consideration / development for industrial applications. More information in this site as soon as feedback is available.
Model animation & validation
- Brama : Event-B model animator initially developped for the Rodin platform. Currently redevelopped for Atelier B 4 and based on PredicateB ++. Distribution would start in 2014.
- ProB : Model-checker developped and distributed by Formal Mind, lightly integrated with Atelier B for proof, animation and data validation.
- PredicateB ++ : B predicate evaluator, part of the Rodin platform, that supersedes previous tool, PredicateB. Provides animation capabilities to Brama.
- BART : automatic refiner tool that allows to generate B machines and implementation components, based on a refinement rules database that can be extended.
- B Compiler : Core tool that allows to parse and analyze full B or Event-B projects.
- Generic proof obligation generator : Upcoming proof obligation generator that provides traceability between models and proof obligations. Theoritical proof obligations can be fully (re)defined. The tool generates a new file format: Bxml.
- Data validation : Validation of a (huge) set of data against a formal data model, modelled using mathematical B language and verification tools like PredicateB++ and ProB.