Présentation

POURQUOI UTILISER L’ATELIER B ?

> Téléchargement Gratuit
> Politique de Distribution
> Contrat de Maintenance
> Enseignement de la méthode B en France

LES NOUVELLES FONCTIONNALITÉS

L’Atelier B 3.7 a subi de nombreuses améliorations et évolutions pour finalement obtenir l’Atelier B 4.
Voici un aperçu des principales évolutions pour cette nouvelle version.

> Disponibilité de l’outil sous Linux, MacOS et Windows grâce au développement de l’interface graphique dans l’environnement Qt et au portage des outils du cœur de l’Atelier B.

> Une 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 (Event-B).

> 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 C (ComenC)

> Support du B événementiel (Event-B) avec contrôles syntaxiques et génération d’obligation de preuve spécifiques

> Ajout d’un moyen d’interfaçage simple et efficace avec des outils externes.