The new formal tool Atelier B 4.7 is available.

18 January 2022

Atelier B 4.7.1 is available in a Community Edition (https://www.atelierb.eu/en/atelier-b-support-maintenance/download-atelier-b/) and in a Maintenance Edition for owners of a maintenance contract.

The main innovations consist in:

  • the addition of an extensible mechanism allowing the integration without recompilation of external mathematical provers (CVC4 and Z3 by default), in order to improve the automatic proof performances. This version is used industrially by Alstom, RATP and Siemens Transportation Systems.
  • the improved support for Event B language for Common Criteria certification (https://www.atelierb.eu/en/atelier-b-4-6-for-eal6/)

The changes planned for 2022 and 2023 concern:

  • security work to comply with EN50128 T2 certification
  • improvement of automatic and interactive proof, by integrating the results of the collaborative R&D projects BLaSST (https://www.clearsy.com/en/research-and-development/blasst/) and ICSPA (https://www.clearsy.com/en/research-and-development/icspa/).
  • an even better support of Event B for Common Criteria certification