PRÉSENTATION : Outil Atelier B

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.

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

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.

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

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.