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 FONCTIONNALITÉS

> 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.

> Un outil de rejeu, le Certifier, certifié T2, permet de garantir la conformité aux normes EN50128 et 50129 des projets développés avec un Atelier B récent.

> Une interface graphique proposant notamment :

• Une vue tout-en-un des projets et de leurs états, une meilleure intégration des messages d’erreur
• un éditeur avec navigation et complétion automatique supportant le langage B et le B événementiel (Event-B).
• 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.

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

> Traducteur d’implémentations B0 vers le langage C (ComenC)

> Traducteur d’implémentations B0 vers le langage Rust (B2rust)

> 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.

> Outil de raffinement automatique (BART)

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