Publié le 19/01/2022 |
L’Atelier B 4.7.1 est disponible en version Community Edition (https://www.atelierb.eu/en/atelier-b-support-maintenance/download-atelier-b/) et en version Maintenance Edition pour les possesseurs d’un contrat de maintenance.
Les principales innovations consistent en :
- l’ajout d’un mécanisme extensible permettant l’intégration sans recompilation de prouveurs mathématiques externes (CVC4 et Z3 par défaut), afin d’améliorer les performances de preuve automatique. Cette version est utilisée industriellement par Alstom, RATP et Siemens Transportation Systems.
- l’amélioration du support du langage B événementiel (Event B) pour la certification Critères Communs (https://www.atelierb.eu/en/atelier-b-4-6-for-eal6/)
L’Agence Nationale de la Recherche (ANR), à travers le projet DISCONT ANR-17-CE25-0005, a contribué au développement de:
- nouvelles fonctionnalités de support de vérification (4.7)
- manuel du B événementiel (ou Event-B) disponible dans la section Aides/manuels (4.7)
- vérification des preuves (4.6)
- utilisation des nombres réels
- ajout uniquement de règle prouvée par PP
- consolidation de la génération des obligations de preuve du NGOP (4.6)
Les évolutions prévues en 2022 et 2023 concernent :
- des travaux de sécurisation en vue d’une certification EN50128 T2
- l’amélioration de la preuve automatique et interactive, par intégration des résultats des projets de R&D collaboratifs BLaSST (https://www.clearsy.com/en/research-and-development/blasst/) et ICSPA (https://www.clearsy.com/en/research-and-development/icspa/).
- un encore meilleur support du B événementiel pour la certification Critères Communs
De plus amples informations sont disponibles dans la note de version 4.7.1.