Version – Atelier B 4.0

Date de diffusion : février 2009
Nouvelles Fonctionnalités / Caractéristiques :

Disponibilité de l’outil sous Linux, Solaris, Mac OS X et Windows grâce au développement de l’interface graphique dans l’environnement Qt et au portage des outils du coeur de l’Atelier B.
Nouvelle interface graphique proposant notamment :
- une vue tout-en-un des projets et de leurs états, une meilleure intégration des messages d’erreur
- l’intégration d’un répartiteur de tâches : les tâches de développement (vérification de type, génération des obligations de preuve, preuve automatique, génération de code) peuvent être réparties sur un parc de serveurs. L’interface permet d’ajouter de supprimer et d’interrompre ces tâches.
- une interface de preuve repensée avec une meilleure gestion de l’arbre de preuve, l’accès simplifié aux commandes de preuve, à l’ajout de règles utilisateurs, à l’analyse syntaxique de formules.
- un éditeur avec navigation et complétion automatique supportant le langage B et le B événementiel
Intégration de la preuve de bonne définition des modèles : création automatique et intégrée d’un projet de bonne définition associé à un projet principal permettant de valider la bonne définition des modèles.
Intégration d’outils de preuve de règles ajoutés plus performants
Ajout d’un outil de raffinement automatique (BART)
Ajout d’un traducteur d’implémentations B0 vers le langage (ComenC)
Support du B événementiel avec contrôles syntaxiques et génération d’obligations de preuve spécifiques.
Ajout d’un moyen d’interfaçage simple et efficace avec des outils externes