Nous avons le plaisir de vous informer de la mise à disposition de la version 4.3.1 de l’Atelier B. Cette version est exclusivement réservée aux détenteurs d’un contrat de maintenance, qui peuvent y accéder depuis la page de connexion.
Outre les 27 correctifs de maintenance, cette version apporte deux nouvelles fonctionnalités en accès anticipé. Il s’agit de l’intégration de l’outil ProB et d’un nouvel outil permettant de vérifier des règles de codage sur les modèles B.
L’intégration de ProB apporte un prouveur dont le comportement est semblable à celui du Predicate Prover mais qui est, de plus, capable de trouver des contre-exemples dans les formules qu’il analyse. ProB est un model-checker pour la méthode B développé à l’université Heinrich-Heine.
Le nouvel outil BCRC (B Coding Rule Checker) a été développé avec le support d’Alstom. Il permet de faire des vérifications de forme sur les modèles B. Ces vérifications permettent notamment de :
- vérifier la présence de suffixes ou de préfixes déterminés sur des paramètres d’opérations ;
- ou de vérifier l’absence d’opérateur ou de substitutions qui seraient interdits dans les règles du codage d’un projet particulier.
Cette version contient 9 règles paramétrables et d’autres règles pourront être ajoutées au besoin. Les résultats de l’analyse peuvent être soit affichés directement dans l’Atelier B pour une visualisation ou correction aisée, soit exportés dans un document.
De plus amples informations sont disponibles dans la note de version