Tools

Several tools (developed, under development or planned to be developed) are discussed in these pages.

Code generation

  • C4bC4B : 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

  • Logo_bramaBrama : 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++PredicateB ++ : B predicate evaluator, part of the Rodin platform, that supersedes previous tool, PredicateB. Provides animation capabilities to Brama.

Model transformation

  • BART : automatic refiner tool that allows to generate B machines and implementation components, based on a refinement rules database that can be extended.

Model analysis

  • 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.

Other topics