Control of coherence between code and specifications

Control of coherence between code and specifications

CLEARSY has the role of “external controller” within the context of developing these projects, undertaking to make an inventory of the various modifications implemented in the specification document and/or B model.

• Our role : External controller

Context

Within the context of developing certain security software products, numerous companies call upon the B Method.

The development of these projects focuses on the drafting of a specification document and a B model enabling the expected software product to be achieved after being translated into the Ada language.

Our actions

CLEARSY has the role of “external controller” within the context of developing these projects, undertaking to make an inventory of the various modifications implemented in the specification document and/or B model. This fairly common practice of requesting an external company to take care of checking the code and its coherence as regards the established specifications is assured within CLEARSY via various activities.

We are able to distinguish between 3 stages during these activities:

• A document – verification report – is drafted, enabling the coherence between the two elements to be accounted for (code and specification), following any modifications carried out.
• Indeed, a model proving activity enables one to ensure that there is no regression following modifications to the principles imposed by use of the B Method.
• Finally, two translations – using two different chains in machine code – are produced, and the comparison of the two results enables the coherence of the generated software to be assured.

We note that these last two stages are specific to the decision to use the B Method.