Atelier B


Atelier B

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.

Ces fonctionnalités se regroupent en quatre 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 projets.

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.

Les commentaires sont fermés.