Atelier B

L’Atelier B est un outil qui permet une utilisation opérationnelle de la méthode B. Il offre, au sein d’un environnement cohérent, de nombreuses fonctionnalités permettant de gérer des projets en langage B.

Fonctionnalités de l’Atelier B

Ces fonctionnalités se regroupent en plusieurs catégories :

• Une aide à la preuve, pour démontrer les obligations de preuve, grâce à des outils de preuve adaptés
• Une aide au développement : gestion automatique des dépendances entre composants B
• Des outils de confort pour l’utilisateur : représentation graphique de projets, affichage de l’état et des statistiques d’un projet, archivage de projet.

Utilisation de l’Atelier B

L’Atelier B s’utilise soit par l’intermédiaire d’une interface Homme Machine au format QT, soit en utilisant directement des commandes (Mode de commandes). L’Atelier B est multi-utilisateurs. Les tâches automatisables lors du développement d’un projet sont les suivantes :

• Vérifications syntaxiques des composants
• Génération automatique des obligations de preuve
• Traduction automatique des implantations B vers les langages C ou Ada.

L’Atelier B est désormais disponible sous Windows, Linux, Mac OS et Solaris.

Accéder au site internet dédié à l’Atelier B.