Couverture de code Caml pour la réalisation d’outils de développement certifiés

Validation dans un contexte certifié

L’aviation civile américaine (FAA) exige pour donner l’autorisation de voler à un avion que tout programme informatique qu’il embarque respecte les normes de développement DO 178B. Selon la criticité du logiciel, c’est-à-dire selon qu’il s’agisse des commandes de vol ou des commandes du lecteur de DVD de chaque fauteuil, cette norme se décline sur plusieurs niveaux (A, B, C, etc.). La DO 178B est très rigoureuse sur les procédures à suivre mais ne donne aucune contrainte sur le langage de programmation à utiliser ni même sur les paradigmes que celui-ci doit suivre. Pour autant, il existe des règles qui viennent préciser cette norme et qui restreignent drastiquement les types de programmes acceptés. Au niveau A qui est le plus haut niveau de criticité, un programme embarqué ne peut faire d’allocation dynamique de mémoire, ni employer de récursion, ni faire quoi que ce soit qui ne soit borné statiquement en temps et en espace avec de surcroît une borne connue. Pour ce genre de développement, l’utilisation de Caml ou de tout autre langage généraliste d’ailleurs, est hors de propos. L’usage est d’utiliser un langage d’assemblage ou des sous-ensembles limités de C ou de ADA.
Cependant, il est permis et de plus en plus indispensable, que ces logiciels soient conçus avec des générateurs de code ou vérifiés avec des outils automatisés ; mais à la condition que ces outils soient eux-mêmes certifiables DO 178B au même niveau de criticité. À titre d’exemple, la mesure de couverture dont nous parlons dans la suite peut être faite manuellement par une relecture indépendante du code ou par un outil si celui-ci se soumet aux exigences de la DO 178B.
Dans le cadre de la réalisation de tels outils, il est admis de « relâcher » les règles les plus contraignantes mais les exigences restent fondamentalement les mêmes. Si par exemple on autorise la récursion ou l’allocation dynamique, il est tout de même requis de circonscrire l’usage de l’outil au domaine où le tas et la pile vont être suffisants pour une utilisation nominale. Même si à la différence d’un programme embarqué, un outil peut échouer dans son exécution, il est indispensable de montrer qu’il ne produira jamais un résultat faux. C’est à ce titre que la phase de validation prend une place prépondérante dans le cycle développement.
Tests : critères de mesure de couverture Dans un processus industriel, la phase de validation prend place après le développement et vise à établir la correspondance entre le produit et sa spécification. On appelle mesure de couverture, la quantification objective de la relation entre une activité de validation et les objectifs qu’elle s’est fixée ; elle est habituellement exprimée comme le pourcentage de l’activité effectué. La finalité de la mesure de couverture est de permettre aux auditeurs de s’assurer que la validation a été menée jusqu’à son terme.
La norme DO 178B définit plusieurs activités de validation et parmi celles-ci plusieurs activités de tests. Une base de tests doit être constituée pour couvrir l’ensemble des spécifications du logiciel qu’on souhaite valider. La mesure de couverture structurelle qui nous intéresse en premier lieu, détermine comment le code est exécuté par cette base de tests et établit la traçabilité entre la structure du code et les cas de tests. Il est demandé par la norme que toute partie du code ait été utilisée dans l’exécution d’un test et que son utilisation ait été conforme aux exigences de la spécification.
Les critères de couverture structurelle se divisent en deux ensembles : ceux sur le flot de données et ceux sur le flot de contrôle. L’analyse du flot de données consiste à caractériser par une métrique particulière le lien entre l’assignation d’une variable et son utilisation. La norme DO 178B n’exige pas de critères particuliers pour la mesure de couverture structurelle du flot de données ; nous allons dans la suite nous focaliser sur celle du flot de contrôle.
Le flot de contrôle est mesuré sur les instructions exécutées, les expressions booléennes évaluées et les branches des instructions de contrôle empruntées. Dans ce qui suit, nous citons les principales mesures.
Couverture des lignes de code (Statement Coverage) C’est sans doute le critère le plus simple à comprendre et à mettre en œuvre, il s’agit de vérifier que pour chaque instruction du programme il existe un test pour lequel cette instruction est exécutée. C’est un critère considéré comme trop faible comme le montre le prochain exemple.
Couverture des décisions (Decision Coverage) On appelle décision, l’expression évaluée dans une instruction de branchement pour décider quelle branche sera exécutée. Classiquement, il s’agit d’une expression booléenne dont il faut s’assurer qu’il existe un test pour lequel sa valeur calculée est true et un autre test où la valeur est false.
L’exemple C suivant illustre la différence entre les deux critères de couverture :
i n t a b s ( i n t x ) { i f ( x < 0 ) x = −x ; r e t u r n x ; }
Un seul test avec une valeur négative suffit pour couvrir toutes les instructions par contre la couverture des décisions nécessite un second test avec une valeur positive pour que la condition (x<0) prenne aussi la valeur false.
Couverture des conditions (Condition Coverage) On appelle condition les sous-expressions atomiques d’une décision. Par exemple, la décision x && (y<0) || f(z) est constituée de trois conditions x, y<0 et f(z). Une condition est couverte s’il existe des tests où cette condition prend les valeurs true et false.
Couverture C/DC (Condition/Decision Coverage) La couverture C/DC cumule les deux précédents critères.
Couverture MC/DC (Modified Condition/Decision Coverage) La couverture MC/DC étend le critère C/DC en introduisant l’exigence que chaque condition doit indépendamment affecter la valeur de la décision. Plus prosaïquement, chaque condition doit recevoir deux tests qui donnent les mêmes valeurs aux autres conditions et qui couvrent la décision par les deux valeurs possibles.
Couverture des conditions multiples (Multiple Condition Coverage) Enfin, il s’agit dans ce critère de fournir des tests pour toutes les combinaisons possibles de valeurs des conditions.
Nous allons illustrer ces définitions par un exemple et par les tests que ces critères de me-
sure requièrent. Nous examinons une instruction de test figurant quelque part dans un programme :
if ((a || b ) && c) { … }. Il existe huit tests différents pour stimuler cette instruction qui sont les huit valuations des trois variables booléennes a, b et c. Nous qualifierons ces valuations et le résultat de l’ex-pression de vecteurs de test et nous les noterons [TTT T], [FTT T], [TFT T], [FFT F], [TTF F], [FTT F], [TFT F] et [FFF F]. Ils correspondent à la table de vérité de l’expression.
Selon le type de couverture mesurée, les tests exigés ne sont pas les mêmes :
– couverture des instructions : un seul test prenant la valeur T est exigé.
– couverture de la décision : deux tests, l’un donnant T et l’autre F, suffisent : par exemple [TTT T] et [FTT F].
– couverture des conditions : chaque condition doit prendre les deux valeurs, donc deux tests qui diffèrent sur toutes les conditions suffisent : [TTF F] et [FFT F] (on note que cet ensemble ne couvre pas la décision).
– couverture C/DC : toujours deux tests qui diffèrent sur toutes les conditions mais qui diffèrent en plus sur la valeur globale : [TTT T] et [FFF F].
– couverture MC/DC : pour chaque condition, il est nécessaire d’exhiber deux tests qui ne diffèrent que pour cette condition et qui font prendre à la décision les deux valeurs de vérité. Par exemple, le couple de vecteurs [TFT T] et [FFT F] montre l’indépendance de la condition a. Les vecteurs peuvent servir pour l’indépendance de plusieurs variables. En général, pour N conditions, il faut N+1 vecteurs de test. Dans cet exemple, quatre vecteurs sont suffisants : [TFT T], [FTT T], [TFF F] et [FFT F].
– couverture des conditions multiples : les huit vecteurs sont nécessaires.
La certification DO 178B au niveau A requiert que l’intégralité du code ait une couverture MC/DC de 100%. Le critère MC/DC est apparu comme un compromis raisonnable entre une exigence trop faible de deux tests et une exigence inatteignable de 2n tests.
La pertinence de la couverture MC/DC est un sujet abondamment débattu[11, 15]. Notre propos est de montrer quel sens cette mesure prend en OCaml sachant que les organismes de certification de l’aviation civile l’exigent. Il faut comprendre que l’analyse MC/DC du code est un des maillons d’un processus qui s’emploie à valider chacune des étapes du développement. Même s’il est théoriquement possible de contourner les analyses de couverture par des « astuces » de codage, en pratique ces « astuces » seront rejetées soit par ceux en charge de la relecture du code, soit par ceux qui valident la mesure MC/DC.

Couverture de code Caml

Comme le disent Chilenski et al.[12], la couverture de code n’est pas un test mais une mesure. Dans cet esprit, nous définissons dans cette section la mesure de couverture pour un programme Caml. Nous poserons les principes de l’analyse des critères MC/DC pour les expressions du langage Caml, en particulier pour la structure de contrôle originale que constitue le filtrage par motif.
Nous avons choisi dans le cadre de cette étude de nous restreindre au noyau fonctionnel et impératif d’OCaml. Nous avons choisi de ne pas traiter les traits les plus modernes du langage mais nous discuterons de leur pertinence dans la conclusion.

Couverture des expressions

Caml est un langage d’expressions : la notion de couverture doit être adaptée en conséquence. En lieu et place de la couverture des instructions nous nous intéresserons à la couverture du calcul des expressions.
Dans un langage impératif, la couverture doit prendre en compte les instructions de contôle pour vérifier indépendamment que chaque branche est exécutée. Avec Caml, la problématique est très similaire avec les constructions du langage où certaines sous-expressions (l’expression conditionnelle par exemple) peuvent ne pas être évaluées.
i f ( x<y ) { l e t min = Au même titre que la couverture du programme
min = f ( x ) ; C mesure quelles sont les branches du if qui ont
i f x<y
} e l s e { été exécutées, la couverture du programme Caml
t h e n f x
min = f ( y ) ; doit examiner quelles sont les sous-expressions de e l s e f y } l’opérateur if qui ont été évaluées.
Une instrumentation du code est nécessaire pour tracer cette information ; elle est légèrement différente de celle réalisée par un outil de profilage (comme ocamlcp) puisqu’ici on ne cherche pas à savoir si un calcul a été atteint mais à vérifier qu’il s’est terminé. Le principe général est de remplacer toute expression expr que l’on souhaite tracer par l’expression (let aux = expr in mark() ; aux) où aux est une variable qui n’est pas libre dans expr et mark une fonction capable par effet de bord de conserver l’information que ce point du programme a été atteint. Sous la réserve que la fonction mark soit indépendante du programme initial et qu’elle termine, l’expression instrumentée et l’expression originale ont le même type et la même sémantique.
Nous formalisons cette transformation en lui adjoignant deux cas particuliers qui sont : si l’expression est atomique (un littéral ou une variable) son évaluation ne peut pas échouer et si l’expression est de type unit, il n’est pas nécessaire de sauvegarder sa valeur. Ces cas particuliers ne sont pas fondamentaux, mais ils permettent d’alléger la transformation.
a −→ mark() ; a où a est un atome
e −→ e ; mark() où e est de type unit
e −→ let aux = e in mark() ; aux
Le cas de l’atome peut être généralisé à toute expression pour laquelle on sait statiquement que son évaluation n’échouera jamais ; c’est-à-dire que son évaluation termine et qu’aucune exception ne peut être levée pendant ce calcul. Sachant que la bibliothèque d’exécution de Caml est susceptible de lever des exceptions, notamment si l’allocation dans la pile ou dans le tas échoue, les expressions satisfaisant cette propriété se limitent principalement au cas des atomes.
À l’exemple de l’opérateur if, un certain nombre de constructions primitives du langage Caml introduisent plusieurs branches de calcul. L’analyse de la couverture des expressions nécessite de tracer l’évaluation de chacune des branches indépendamment des autres. Pour éviter le « sur-marquage », on décompose cette instrumentation par deux transformations qui explorent l’arbre de syntaxe d’une expression. La transformation G parcourt l’arbre et appelle F sur les sous-expressions que l’on souhaite marquer. À l’inverse, la transformation F parcourt l’arbre et appelle G sur les sous-expressions que l’on ne désire pas marquer mais dont on souhaite marquer les éventuelles branches.
F(a) = mark() ; a si a est un atome ou une variable
F(e1 e2) = let aux = G (e1) G (e2) in mark() ; aux
F(fun x -> e) = mark() ; fun x -> F(e)
F(e1 ; e2) = G (e1) ; F(e2)
F(if e1 then e2 else e3) = if G (e1) then F(e2) else F(e3)
F(while e1 do e2 done) = while G (e1) do F(e2) done ; mark()
F(for x = e1 to e2 do e3 done) = for x = G (e1) to G (e2) do F(e3) done ; mark()
F(match e with p1 -> e1 | … | pn -> en) = match G (e) with p1 -> F(e1) | … | pn -> F(en)
F(let x = e1 in e2) = let x = G (e1) in F(e2)
F(try e with p1 -> e1 | … | pn -> en) = try F(e) with p1 -> F(e1) | … | pn -> F(en)
La principale différence entre les deux est que seule F marque la fin du calcul d’une expression ; les deux instrumentent toutes les branches contenues dans l’expression traduite.
G (a) = a
G (e1 e2) = G (e1) G (e2)
G (fun x -> e) = fun x -> G (e)
G (e1 ; e2) = G (e1) ; G (e2)
G (if e1 then e2 else e3) = if G (e1) then F(e2) else F(e3)
G (while e1 do e2 done) = while G (e1) do F(e2) done
G (for x = e1 to e2 do e3 done) = for x = G (e1) to G (e2) do F(e3) done
G (match e with p1 -> e1 | … | pn -> en) = match G (e) with p1 -> F(e1) | … | pn -> F(en)
G (let x = e1 in e2) = let x = G (e1) in G (e2)
G (try e with p1 -> e1 | … | pn -> en) = try G (e) with p1 -> F(e1) | … | pn -> F(en)
Comme les autres opérateurs (accesseurs, affectation, etc..), les opérateurs booléens ne sont pas détaillés dans ces transformations mais traités comme des applications ce qui suffit à établir leur couverture simple. Nous verrons dans la section 3 le traitement particulier qui leur est réservé dans le cadre d’une analyse MC/DC de la couverture.
Récursion terminale La récursion terminale n’est pas une spécificité d’OCaml ou des langages fonctionnels. C’est une propriété des appels récursifs d’une fonction qui est exploitée par les compilateurs pour optimiser le code objet généré. Cette optimisation s’applique lorsque l’appel récursif d’une fonction est la dernière opération exécutée de cette fonction et consiste à remplacer le mécanisme d’appel classique par un simple branchement. Elle permet d’une part d’accélérer le code produit mais surtout d’économiser de l’espace dans la pile d’appel.
L’instrumentation que nous proposons, consistant à ajouter un effet de bord spécifique à la trace après chaque expression, brise systématiquement l’appel terminal et interdit l’optimisation. Ainsi, le programme instrumenté pourra nécessiter plus d’espace mémoire sur la pile d’exécution que le même programme non instrumenté.
En conséquence, les tests nécessaires à la couverture devront être choisis de sorte à ne pas faire exploser la pile. Quand ceci n’est pas possible, il devient nécessaire de dérécursiver le code.
Correction de l’instrumentation Sachant que mark() est de type unit, les transformations opérées par les fonctions F et G ne modifient pas le type de l’expression traduite.
Dans le même ordre d’idée, ces transformations ne font que rajouter mark() à certains endroits de l’expression. Il est facile de montrer que l’ajout de cet effet de bord ne modifie pas la valeur calculée par l’expression initiale.
La couverture d’une application est mesurée par l’examen des traces construites lors de l’exécution des fonctions mark introduites par la tranformation F appliquée à l’ensemble du code. Donc, un programme est couvert à 100%, si et seulement si, il existe des tests couvrant toutes les marques.

Couverture MC/DC

Il n’existe par réellement une définition précise de la couverture MC/DC ; cette notion est toujours plus ou moins dépendante du langage sur lequel elle s’opère et de l’outil que l’on utilise. En particulier, la notion de MC/DC est définie sur les expressions booléennes mais la couverture est effectuée sur les instructions de branchement.
Le point de vue adopté pour OCaml est différent. Nous ne nous intéressons pas à l’aspect syntaxique des expressions mais à leur type. Toute expression de type bool est analysée et instrumentée pour en mesurer sa couverture MC/DC et ce quelque soit le lieu où cette expression prend place. Une exception est faite pour les littéraux booléens true et false.
Décomposition d’une expression Le typage des expressions permet de caractériser les décisions ; une analyse de la structure de l’expression nous permet ensuite de préciser les conditions qui la composent. Nous nous contenterons d’isoler les arguments des opérateurs booléens not, && et ||. Par exemple :
a && (f x) || not (b || c) est composé de quatre décisions : a, (f x), b et c.
L’instrumentation d’une décision doit conserver la sémantique de l’expression initiale. Les conditions n’étant pas obligatoirement des expressions fonctionnelles pures, l’instrumentation du code doit conserver l’ordre d’évaluation des conditions.
Nous proposons une transformation des expressions booléennes qui fait apparaître explicitement les différentes branches de calcul de cette expression et par la même, le vecteur correspondant à chaque branche.