Click here for English.

LE DAB EN QUELQUES CHIFFRES

L'état global du projet, obtenu avec la version 2.9 de l'Atelier B, est représenté par le schéma ci-dessous :

Evaluation quantitative

• Nombre de composants :
  Le projet B associé au DAB comporte 38 composants (machine abstraite et implantation), dont 7 machines de base spécifiquement développées.

• Nombre de lignes de code :
  - Le modèle B compte environ 3700 lignes de B,
  - Le code C généré par l'Atelier B comporte 3200 lignes (fichiers header et de code C),
  - Le code Ada généré par l'Atelier B comporte 5800 lignes (fichiers de spécification et de code Ada).

• Nombre d'Obligations de Preuve :

  Le projet B compte, pour l'ensemble de ces composants :

  - 3960 Obligations de Preuve triviales ; c'est à dire directement démontrées par l'Atelier B. Aucun travail de preuve n'est à réaliser pour de telles obligations de preuve,
  - 839 Obligations de Preuve non triviales à démontrer; ces dernières ont été démontrées automatiquement ou de façon interactive en indiquant au prouveur les tactiques de preuve à appliquer.

Evaluation qualitative

• Architecture du Projet :

  Les spécificités du projet DAB sont les suivantes :

  - Le projet B associé au DAB ne comporte aucun raffinement. Les structures de données manipulées et les algorithmes décrits dans le corps des opérations étant suffisamment clairs, il n'a pas été nécessaire d'introduire des raffinements de données ou algorithmiques.

  - Les clauses d'architecture utilisées sont de type INCLUDES, SEES et IMPORTS. Les liens de type SEES sont peu nombreux, ceci afin d'améliorer la lisibilité et la maintenabilité des composants. Ces liens sont créés pour consulter des composants de contexte (définissant les ensembles et les constantes).

  Les liens de type INCLUDES sont utilisés sur des composants de contexte.

• Taux de couverture de preuve :

  Le taux de couverture de preuve correspond au pourcentage d'Obligations de Preuve démontrées par rapport au nombre total d'Obligations de Preuve (non triviales) générées.

  - Le taux de couverture de Preuve obtenu par l'utilisation du Prouveur Automatique est de 93%(soit 787 Obligations de Preuve déchargées),
  - L'utilisation du Prouveur Interactif (sans ajout de lemmes utilisateur) améliore ce taux de couverture de 6%,
  - Un seul lemme utilisateur a été rajouté,
  - Le projet DAB est prouvé à 100%.

  Généralement, le taux de couverture de preuve obtenu par l'utilisation du Prouveur Automatique seul, est d'environ 70%. On estime qu'au dessous de 50%, le projet B nécessite d'être remanié (soit en décomposant les modules B, soit en introduisant des raffinements, soit encore en exprimant le besoin autrement).

  Les performances du prouveur automatique sur le projet DAB peuvent s'expliquer par les raisons suivantes :

  - l'utilisation de structures de données simples (booléens, tableaux) facilement manipulables par le prouveur,
  - les calculs arithmétiques sont peu nombreux (donc il y a peu d'obligations de preuve vérifiant le non débordement),
  - la décomposition obtenue par les liens IMPORTS permet non seulement de découper le modèle B en activités spécifiques, mais aussi de découper le travail de preuve. Les Obligations de preuve générées sont, de ce fait, plus simples et moins nombreuses (apparition d'obligations de preuve triviales).