Accueil - Nouveautés - Produit - Versions - Télécharger - Manuels - Maintenance - Politique de Distribution
Perspectives & Appels à Contribution - Support - Formation - Documents - Presse - Références -
R&D - Contacts - Emploi - Liens - Votre Compte

L'Atelier B

Présentation

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 principales fonctionnalités de l'Atelier B

Les langages supportés

B
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 contextuelles dont le contrôle de type et le contrôle de portée des identificateurs. Le passage d'un composant au travers du Type Checker est un requis avant sa preuve et avant d'autres vérifications présentées ci-dessous,
le B0 Checker effectue des 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 être sauvegardés aux formats pdf, rtf et LaTeX.

Les outils de preuve

Les fonctionnalités suivantes :

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

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.

La gestion de projets

L'Atelier B offre des services de gestion de projets de 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.
intégration du "Paralléliseur" : une application permettant de lancer sur des machines distantes partageant le même système de fichiers des tâches de preuves sur un projet B. (pour Unix et Linux uniquement)