Appuyer ici pour la version francaise.

DEVELOPMENT CYCLE SOFTWARE

The Development Cycle software followed is shown below.

Identification of the requirements

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.

Entry document :

• The Requirements document

Exit documents :

• the Requirements document with annotations corresponding to the requirements,
• the first column of the Tracing Matrix of the requirement.

Functional specification file

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.

Entry documents:

• The annoted Requirements document,
• The tracing matrix

Exit documents

• The functional Specification file made up of SADT boards,
• The tracing matrix comprising another column giving reference for each requirement in the functional model,
• The validation file constituted of the tests scenarii specifications. Those must cover the totality of the identified requirements in the Textbook of Charges.

Specification and Formal Conception

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.

Methodology used for the construction of the formal specification model.

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.



Methodology for the formal verification

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.

Entry document:

• The Functional Specification File
• The tracing matrix

Exit documents:

• The B model constituted of B modules (abstract machines and implementations).
• The tracing matrix comprising an added column giving reference for each requirement in the B model.

Generation of the computing code of the B model

The use of translation platforms of the Atelier B makes this step automatic.

This step computing code generation is split into two phases:

• a coding activity of the base machines. Let's recall that the implementations only are translated. The basic machines of the application (interfaces with the outside) are abstract machines and their computing code must be written manually. To avoid the interfacing problems, implementations said "empty shells" are written then translated automatically, the associated computing code is simply added to them during the coding phase of basic machines.
• a coding activity made automatic with the use of translation platforms of the Atelier B.

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.

Entry documents:

• The totality of the B model components.

Exit documents:

• The computing code associated with the B model.

Test stages

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.