PRÉSENTATION : Outil Atelier B

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

SES FONCTIONNALITÉS SE REGROUPENT EN 4 CATÉGORIES

1- Une aide à la preuve, pour démontrer les obligations de preuve, grâce à des outils de preuve adaptés.

2- Une aide au développement, pour gérer automatiquement les dépendances entre composants B.

3- Des outils de confort pour l’utilisateur, avec la représentation graphique de projets et l’affichage de l’état et des statistiques d’un projet, archivage de projets.

4- Interface utilisateur : l’Atelier B s’utilise soit par l’intermédiaire d’une Interface Homme Machine développée avec 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 disponible sous les systèmes d’exploitation Windows, Linux et MacOS.

LES PRINCIPALES FONCTIONNALITÉS DE L’ATELIER B

LES LANGAGES SUPPORTÉS

B et B évènementiel.

LE RAFFINEMENT AUTOMATIQUE

Intégration d’un outil de raffinement automatique (BART).
BART permet de générer raffinement et implémentation à partir d’une base de règle de raffinement extensible par l’utilisateur. BART fonctionne sur une base de règles de raffinement. Des règles de raffinement supplémentaires peuvent être ajoutées afin de permettre la personnalisation du raffinement de certains composants.

 

LES ANALYSEURS SYNTAXIQUES

Ils permettent d’effectuer l’ensemble des vérifications syntaxiques sur les fichiers en langage B :

  •  un éditeur de modèle a été intégré à l’Atelier B. Celui-ci intègre un analyseur syntaxique, la complétion automatique ainsi que des fonctionnalités de navigation au travers du modèle.
  • le Type Checker effectue d’abord la vérification grammaticale d’un composant B, et ensuite un certain nombre de vérifications spécifiques au langage B0 utilisées dans les implantations (une sous-partie du langage B) pour assurer que celles-ci peuvent être traduites.
  • Le vérificateur de projets effectue des vérifications sur l’ensemble des composants d’un projet pour contrôler son architecture (les liens entre les composants). La vérification d’un projet est un requis avant la traduction finale du projet.
    Les modèles B peuvent êtres sauvegardés aux formats pdf, rtf et LATeX.

LES TRADUCTEURS AUTOMATIQUES

Les implantations constituent l’étape de codage d’un développement en langage B. Elles sont écrites à l’aide d’un sous-ensemble du langage B, similaire à un langage de programmation impératif. Afin de faciliter la génération de code sur n’importe quel système cible, les implantations sont traduites automatiquement en langage de programmation classique. Les programmes obtenus peuvent alors être compilés et assemblés sur la machine cible pour produire le logiciel exécutable.

LA REPRÉSENTATION GRAPHIQUE DES PROJETS

Elle permet de représenter graphiquement les composants d’un projet et leurs liens, en les positionnant automatiquement au sein du graphe.

L’utilisateur peut choisir différentes options d’affichage, comme la nature des liens à visualiser, la visualisation du graphe de dépendance complet d’un projet ou du graphe de dépendance d’un composant.

LES OUTILS DE PREUVE

  •  La génération automatique des obligations de preuve à partir des composants en langage B.
  • Un composant B est correct lorsque ses obligations de preuve sont démontrées.
  • La preuve en mode automatique : sans intervention de l’utilisateur, la plupart des obligations de preuve sont démontrées.
  • La preuve en mode interactif utilisée lorsque le mode automatique a échoué : l’utilisateur guide le prouveur dans sa démonstration d’une obligation de preuve à l’aide de commandes interactives (ajout de lemmes, preuve par cas…).
  • Le prouveur des prédicats : démonstration de prédicats : démonstration des règles ajoutées par l’utilisateur.
  • La visualisation des obligations de preuve, leur origine et leur état (triviales, prouvées, non prouvées).
  • La gestion d’une base de règles validée comprenant plus de 2.200 règles.

LA GESTION DE PROJETS

L’Atelier B offre des services de gestion de projets en grande taille (comprenant par exemple 500 composants).

En particulier :

  • l’utilisation de l’Atelier B par plusieurs utilisateurs en réseau. Ces utilisateurs peuvent travailler en même temps sur le même projet,
  • d’archiver et de restaurer un projet complet,
  • d’architecturer un projet en plusieurs sous-projets ou bibliothèques.
    L’Atelier B permet ainsi des développements importants et modulaires, par plusieurs équipes de développeurs,
  • de visualiser de manière synthétique l’état d’un projet, en fournissant pour chaque composant, son état (passé au Type Checker, traduit en C ou en Ada), le nombre d’obligations de preuve et le pourcentage prouvé,
  • de générer automatiquement les dépendances entre composants d’un projet; Ainsi, pour effectuer une action (passage au Type Checker, au Générateur d’obligations de preuve…) sur une sélection de composants, l’Atelier B reporte la ou les actions nécessaires sur les composants dont ils dépendent
  • de s’interfacer avec les outils de gestion de version,
  • de vérifier des règles de codage.