Vérification de cohérence entre code et spécifications

Vérification de cohérence entre code et spécifications

CLEARSY occupe dans le cadre du développement de ces projets le rôle de “vérificateur externe”, en se chargeant de recenser les différences modifications opérées sur le document de spécification.

• Notre rôle : Vérificateur externe

Contexte

Dans le cadre du développement de certains produits logiciels sécuritaires, de nombreuses sociétés font appel à la méthode B.

Le développement de ces projets est axé sur la réaction d’un document de spécification et d’un modèle B permettant d’aboutir, après traduction en langage Ada, au produit logiciel attendu.

Nos actions

CLEARSY occupe dans le cadre du développement de ces projets le rôle de “vérificateur externe”, en se chargeant de recenser les différentes modifications opérées sur le document de spécification et/ou le modèle B. Cette pratique, assez courante de demander à une entreprise extérieure le soin de vérifier le code et sa cohérence vis-à-vis des spécifications établies, est assurée au sein de CLEARSY via différentes activités.

Nous pouvons distinguer 3 étapes lors de ces activités :

• Un document “rapport de vérification” est rédigé, permettant de rendre compte de la cohérence entre les deux éléments (Code et spécification), suite aux modifications effectuées.
• Par ailleurs, une activité de preuve du modèle permet de s’assurer qu’il n’y ait pas régression suite aux modifications vis-à-vis des principes imposes par l’utilisation de la méthode B.
• Enfin, deux traductions utilisant deux chaînes différentes en code machine sont produites, et la comparaison des deux résultats permet de s’assurer de la cohérence du logiciel généré.

Notons que ces deux dernières étapes sont spécifiques au choix de l’utilisation de la méthode B.