Publié le 20/01/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 Agence Nationale de la Recherche (ANR), with the project DISCONT ANR-17-CE25-0005, contributed to the development of:
- new verification support features (4.7)
- Event-B manual available in the section Help/Manuals (4.7)
- proof verification (4.6)
- support of real numbers utilisation des nombres réels
- addition of rules only proved by PP
- consolidation of the proof obligations generation of the NGOP (4.6)
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
If you require more detailed information please refer to the 4.7.1 release notes