Appuyer ici pour la version francaise.
The Development Cycle software followed is shown below.
This step consists in listing the totality of the requirements listed in the Requirements document (functional requirements and operational constraints).
Each of the requirement is referenced in the Requirements document, it is noted [Exx] where xx is the requirement number. The requirements which can be deducted from requirements already referenced are not introduced.
This step consists of proposing a functional model in the form of SADT boards (decomposition in several activities). This model takes part in the elaboration of the B formal specification.
This step permits the construction of the B model, from the SADT boards of the functional Specification File.
The formal specification step consists of constructing a first B model from the SADT boards of the Formal Specification file.
The Formal Conception step then consists in refining the first model and takes place when all implementations are obtained.
We will describe the method used for the Formal Specification step; for more information you can refer to the Methodological Information rubric Methodological informations.
Each activity described in the SADT boards becomes a B operation; it remains to establish in which B components these operations are defined.
Given the following example: in a control/command software the main activity (ie. a processing cycle) is decomposed by a data acquisition activity, a processing activity and finally an emitting phase of results.
The activity of higher level is in fact decomposed in three sub-activities. In the same way, the B operation of higher level, corresponding to the processing cycle, uses the B operations dedicated to data acquisition, and the processing of this data and finally the issuing of results.
Each activity present in the above drawing is transformed in a B operation. The modelisation obtained is shown in the drawing below.
The construction of the model is accompanied by a formal verification step : the Proof Obligations produced must be demonstrated.
The automatic prover is used for each component, to demonstrate the Proof Obligations. The remaining POs are verified "visually", the developer simply notes the demonstration allowing confirmation of the validity of the PO, for each proof obligation still remaining to demonstrate. The interactive proof task is not realised during this step.
When the B model is entirely constructed and when all proof obligations still to be proved are verified, the task of interactive proof can begin.
The use of translation platforms of the Atelier B makes this step automatic.
This step computing code generation is split into two phases:
The first step can be accompanied by preliminary tests accomplished on the translated B model. The "empty shells" of the basic machines implementations specify selected tests (for the basic machine associated with the banking card, the empty shell specifies a code, a validity date, the maximum amount of withdrawal...). These implementations are translated automatically and permit the generation of a complete executable. We verify in such way, by modifying the information contained in the implementations of the basic machines, then by regenerating the executable, that the translated B model is behaving normally. This proto-typing phase will be completed by the use of the Animator of the Atelier B. This tool realises the symbolic execution of a software component, from a part of the B model or of the totality of the model.
The proto-typing or animation step is important since it enables to detect the possible problems of formalisation (taking bad account of the system's requirements) or the non-said in the Requirements document.
Only the unitary tests of the code associated with the basic machines and the Man Machine Interface are realised on the DAB project.
The preliminary tests show that the software produced from the B model (in its totality) are behaving correctly.
The integration tests show the validity of the interfaces between the different software components; the interfaces between the software components issued from the B model are correct, only the interfaces between the B and non B components are tested.
The integration and validation tests are identical to those realised for a classic development. The validation tests are executed on the complete software, the tests scenarii must cover the totality of the requirements; to that end a tracing matrix is provided.