Appuyer ici pour la version francaise.

FACTS AND FIGURES ABOUT THE PROJECT

The global state of the project is shown below :

Quantitative evaluation

• Number of components:
The B project associated with the DAB comprises 38 components (abstract machine and implementation), of which 7 basic machines specifically developed.
• Number of coding lines:
  - The B model counts about 3700 lines of B,
  - The C code generated by the Atelier B comprises 3200 lines (header files and of C code),
  - The Ada code generated by the Atelier B comprises 5800 lines (files of specifications and of Ada code).

• Number of Proof Obligations:
  The B project counts, for the totality of its components:
  - 3960 trivial Proof Obligations; ie. directly demonstrated by the Atelier B. No proof work is to be realised for such proof obligations,
  - 839 non trivial Proof Obligations to demonstrate; the latter have been demonstrated automatically or interactively by indicating to the prover the proof tactics to apply.

Qualitative evaluation

• Architecture of the Project:

  The specifics of the DAB project are the following:

  - The B project associated with the DAB does not comprise any refinement. The structures of the manipulated data and the algorithms described in the body of operations being sufficiently clear, it hasn't been necessary to introduce any data or algorithmic refinements.

  - The architecture clauses used, are of INCLUDES, SEES and IMPORTS types. The links of SEES type are very few, this in order to improve the readability and maintainability of the components. These links are created to consult context components (defining the ensembles and constants).

  The links of INCLUDES type are used on context components.

• Proof coverage rate:

  The proof coverage rate corresponds to the percentage of Proof Obligations demonstrated in comparison to the total number of generated Proof Obligations (non trivial).

  - The proof coverage rate obtained by the use of the Automatic Prover is of 93% (ie. 787 acquitted Proof Obligations),
  - The use of the Interactive Prover (without adding user lemma) improves this coverage rate by 6%,
  - Only one user lemma has been added,
  - The DAB project is 100% proved.

  Generally, the proof coverage rate obtained by the use of the Automatic Prover only, is of approximately 70%. It is estimated that below 50%, the B project necessitates rehandling (either by decomposing the B modules, or by introducing refinements, or by expressing the need in another way).

  The performances of the automatic prover on the DAB project can be explained as follows:

  - the use of simple data structures (booleens, arrays), easily manipulated by the prover,
  -the arithmetic calculations are very few (thus there are few proof obligations verifying the non dissipation),
  - the decomposition obtained by the IMPORTS links permits not only to divide the B model in specific activities, but also to divide the proof work. The Proof Obligations generated are, as such, more simple and less in number (appearance of trivial proof obligations).