Grammaire informelle des expressions du langage mCaml

Télécharger le fichier pdf d’un mémoire de fin d’études

Processus de certification (ou de qualification)

Le processus de certiVcation (ou de qualiVcation [44] [45], c’est une question de vocabulaire qui varie selon le domaine et l’objet concerné) d’un logiciel critique consiste en pratique à rassembler les responsables du projet et les représentants des autorités de certiVcation pendant plusieurs jours aVn de passer en revue toute la documentation de l’ensemble du processus, pour vériVer que tout a bien été respecté.
Cela implique donc que l’ensemble du processus de développement est directement impacté par le processus de certiVcation, puisque s’il ne l’a pas pris en compte, le résultat ne peut pas passer la certiVcation. Kornecki et Zalewski [47] présentent un état de l’art en 2009 du processus de certiVcation appliqué aux diUérents objets logiciels (e.g., générateur de code, outil de vériVcation du code, logiciel critique embarqué) intervenant dans le cadre d’un développement de logiciels pour l’avionique civile.
On remarque que l’autorité de certiVcation ne lit pas le code du logiciel ou du moins pas exhaustivement.
Elle regarde surtout comment il a été produit et comment il a été vériVé. La vériVcation de la traçabilité entre le code et la conception détaillée par l’autorité pourra impliquer de prendre du code et vériVer sa provenance, ainsi que dans l’autre sens de prendre une exigence et vériVer son implantation.
Cela ne veut pas dire que personne n’a relu le code. Par exemple, si des règles de codage (e.g., interdiction d’allocation dynamique) interviennent dans le processus de développement, un document doit attester que ces règles ont été respectées.

Évolution des coûts

Selon Myers en 1979 [62], le temps passé dans les activités de tests pour un logiciel était d’environ
la moitié du temps total de son développement, pour un coût dépassant un peu la moitié du coût total.
Environ trois décennies plus tard, Myers et al. ont conVrmé ces chiUres à deux reprises, en 2004 [64] .

Évolution des techniques

Pourtant ces 30 dernières années, les techniques de tests ont évolué, permettant ainsi la réduction
des coûts des tests. C’est le cas aussi pour ce qui concerne les environnements de développement de manière générale.
Mais dans le même temps, les logiciels sont devenus beaucoup plus complexes, ce qui explique en
bonne partie que les coûts des activités de tests ont gardé la même proportion.
D’autre part, les auteurs de livres sur l’activité de tests aXrment tous qu’il y a très peu de formations
aux tests dans les écoles et universités.

Outils pour la couverture de code

Pour mesurer la couverture de code, l’utilisation d’outils est devenue indispensable du fait de la taille et de la complexité des programmes développés de nos jours. De nombreux outils existent pour les langages les plus utilisés dans le monde des logiciels critiques, que sont le langage C [36] [65] et le sous-ensemble SPARK [2] du langage Ada.
Le travail mené au cours de cette thèse a été précisément de concevoir et réaliser un outil permettant l’utilisation d’une autre sorte de langage, précisément OCaml, dans le processus de développement d’un logiciel critique pour l’avionique civile. Ce travail prend son origine dans une collaboration avec la société Esterel Technologies que nous présentons brièvement à la section suivante.
Dans cette section, on résume l’expérience de l’entreprise Esterel Technologies avec OCaml utilisé en tant que langage d’implantation du générateur de code de SCADE, présentée dans les articles [68][66][67].
Ce travail avait été eUectué en partenariat avec les laboratoires PPS et LIP6.
L’entreprise Esterel Technologies développe et commercialise SCADE, un environnement de développement d’applications critiques. Les applications sont développées en langage Lustre puis traduites automatiquement en langage C. (Quelques références sur le langage Lustre : [35] [34] [12].) La suite SCADE oUre la possibilité de programmer en langage graphique Scade (à la place d’écrire du code Lustre). Le processus de traduction du Scade vers C est réalisé par le générateur de code appelé KCG11.
Pour passer à la version 6 de SCADE, Esterel Technologies a développé en OCaml un prototype de KCG [30]. La société a choisi de garder le même langage d’implantation pour passer du prototype à la nouvelle version de KCG. Le langage choisi pour développer le prototype (OCaml) facilite la traçabilité entre la spéciVcation du générateur de code et son implantation. Cela tient au fait qu’un générateur de code est un programme de manipulation d’arbres de syntaxe abstraite, et que les langages de la famille ML, dont fait partie OCaml, oUre des facilités pour ce genre de traitements (type somme, Vltrage par motifs).

Le langage mCaml

Notre langage est entièrement déVni formellement mais pour alléger sa présentation, celle-ci est découpée en deux. Cette section présente une grammaire simpliVée des expressions du langage et unit qui est utilisée.

Le langage mCaml

donne la sémantique opérationnelle des déVnitions globales et des expressions du langage. La sémantique opérationnelle n’est déVnie que pour les programmes acceptés par le système de types qui est déVni en annexe (section A.2, page 161). En annexe, se trouve également la grammaire formelle et complète du langage en section A.1 (page 157). Nous insistons sur la nécessité de la présence d’une déVnition formelle, d’autant plus que nous proposons un langage peu conventionnel notamment dans l’optique de l’utiliser dans un cadre de développement de logiciels critiques, comme pourraient le rappeler Halang et Zalewski [33].

Grammaire informelle des expressions du langage mCaml

Nous donnons ici une grammaire sous forme intuitive dans le but de permettre au lecteur de se faire rapidement une idée du langage que nous déVnissons.
La Vgure III.1 résume les expressions du langage mCaml, où x désigne une variable, c désigne une constante, e désigne une expression, f désigne un champ d’enregistrement, C désigne un constructeur constant (i.e., valeur d’un type énuméré), C(e) est un constructeur ayant un argument (i.e., valeur d’un type énuméré associée à une autre valeur) et p désigne un motif servant au Vltrage. Les mots-clefs du langage sont en gras.

Sémantique opérationnelle du langage mCaml

Cette section décrit comment un programme écrit en mCaml s’évalue. Nous utilisons la sémantique
opérationnelle à grands pas. mCaml, à l’instar d’OCaml, utilise la convention d’appels par valeurs, c’est-à-dire que lors d’une application, l’argument d’une fonction est évalué avant le corps de la fonction.
En OCaml, il n’est pas spéciVé l’ordre d’évaluation des paramètres des fonctions. Ainsi, dans l’évaluation de l’expression (foo (raise A) (raise B)), il est diXcile de savoir si c’est l’exception A ou l’exception B qui sera levée. Cette sémantique laisse la liberté au compilateur (ou à son concepteur) de décider qui évaluer en premier pour des questions d’optimisations. En mCaml, il n’est pas question d’optimisations du compilateur. La sémantique de mCaml ne laisse aucun choix ouvert.

Spécification de la couverture des expressions pour mCaml

Dans cette section, nous déVnissons formellement le critère de couverture structurelle de code simple pour le langage mCaml.
Le principe est le suivant : une expression atomique (constantes et variables) est couverte si elle est évaluée ; pour toutes les autres expressions, qui comportent toutes une ou plusieurs sous-expressions, il faut pour être couverte que chacune des sous-expressions soit couverte, et qu’en plus, sauf impossibilité totale, elle soit évaluée en une valeur. Un exemple d’impossibilité totale d’évaluation en une valeur : (raise e). En eUet, (raise e) ne peut, par déVnition, s’évaluer en une valeur.
Intuitivement, nous souhaitons que le taux de couverture soit de 100% pour un programme qui s’évalue sans problème et dont on ne peut pas améliorer la couverture en ajoutant des tests ou en modiVant des branchements conditionnels.

Règles formelles de couverture des expressions pour mCaml

On établit la couverture de code à partir d’un ensemble d’arbres d’évaluation noté TR et obtenu à partir d’un ensemble de jeux de tests. Un arbre d’évaluation résulte de l’évaluation d’un programme d’après sa sémantique opérationnelle, à partir d’un jeu de tests, comme déVni plus haut.
Le prédicat C est déVni ci-après inductivement. Il prend une expression en argument et aXrme sa couverture. Les expressions non-couvertes ne satisfont donc pas les règles.
Une constante est couverte si, et seulement si, elle apparaît dans une feuille d’un des arbres d’évaluation.
Ici, « une constante » désigne précisément une constante apparaissant à un endroit précis dans le
code du programme. Par exemple, si la constante 42 apparaît plusieurs fois dans un programme, chacune de ses occurrences aura sa propre mesure de couverture. CC ? 9T 2 TR  (E;M` c ;v M) 2 T TR ` C(c).

Critères de couverture pour les expressions booléennes

Cette section porte sur les critères de couverture conditionnelle classiquement rencontrés dans la littérature. Nous gravirons une échelle de complexité en partant d’un critère simple, celui de la couverture des conditions, pour arriver au fameux critère MC/DC.
Les déVnitions proposées dans cette section ne portent pas particulièrement sur mCaml, mais plutôt sur les langages de programmation en général. Ces déVnitions serviront alors de base et lorsque ce sera nécessaire, elles seront raXnées. D’autre part, les notions de « condition » et de « décision » utilisées dans cette section sont « génériques », en ce sens que quelles que soient les variantes des déVnitions utilisées pour ces deux mots, les déVnitions proposées dans cette section ne devraient pas en être impactées.
On peut toutefois aXrmer que dans tous les cas, une condition et une décision sont des expressions booléennes.
Les valeurs booléennes ne sont pas les mêmes dans tous les langages. En C, un mot (e.g., un entier, un Wottant, une adresse mémoire) dont tous les bits sont à 0 représente faux, et tous les autres mots représentent vrai. En Java, nous avons les valeurs primitives true et false, comme pour ML.
En même temps, on peut dire que le type des booléens est représenté et représentable par deux ensembles de valeurs (qui sont souvent chacun des singletons mais pas toujours). Ici, on choisit eUectivement de ne considérer que les deux valeurs true et false.

Couverture des conditions/décisions modifiée (MC/DC)

Intuitivement, le critère MC/DC demande, en plus de C/DC, à ce que les conditions d’une décision donnée puissent chacune avoir un eUet sur la décision. Ce critère sert à donner une preuve que toutes les conditions servent. Les conditions qui ne satisfont pas ce critère sont suspectes ; le cas le plus simple où cela arrive est une décision où la même condition apparaît plusieurs fois dans une décision (e.g., (x && x)). Il faut alors soit justiVer la présence des conditions qui ne satisfont pas le critère ou bien mener une nouvelle campagne de tests.
Ce critère est sujet à de nombreuses interprétations, certaines plus eXcaces que d’autres pour la détection des erreurs, certaines plus coûteuses que d’autres. Les diUérentes interprétations seront souvent un compromis entre eXcacité et coût.
Hayhurst et al. proposent un tutoriel sur ce critère de couverture de code [38].
Les membres de CertiVcation Authorities Software Team (CAST) ont publié leur point de vue [13] sur l’interprétation de la notion de « décision ».
Chilenski étudie l’eXcacité de trois interprétations de ce critère dans [14].
Comme ce critère est complexe et important notamment pour les projets soumis aux obligations de la DO-178B, on va développer davantage les motivations.

Au plus « 2n tests pour le critère MC/DC »

Quand on rattache des conditions à une décision, usuellement il s’agit d’utiliser des opérateurs booléens de conjonction et de disjonction, qu’ils soient séquentiels ou non. On peut bien sûr rencontrer d’autres opérateurs logiques tels que la disjonction exclusive par exemple.
Plus loin dans ce chapitre (sections IV.2.4, page 77 et IV.2.5, page 78), nous proposerons de rattacher les conditions à une décision selon des moyens plus généraux que les opérateurs logiques. Par exemple, on peut se poser la question de la diUérence fondamentale entre un opérateur logique de conjonction (&&) et la construction conditionnelle (if), puisque le premier peut être remplacé par le second : e1 && e2 ; if e1 then e2 else false.
Avec les opérateurs logiques séquentiels, certaines conditions sont inatteignables dans certaines conVgurations (e.g., (e1 && e2) où e1 s’évalue en false).
De manière plus générale, si pour un ensemble de conditions d’une décision, une seule condition peut être évaluée (c’est le minimum puisque sinon la décision ne prend pas de valeur) à la fois, le nombre de tests nécessaires devient 2n pour une décision à n conditions. En eUet, pour que chaque condition soit évaluée aux deux valeurs booléennes, d’une part il faut deux tests par condition et d’autre part chaque condition aUecte forcément la décision indépendamment des autres puisque les valeurs des autres ne sont pas calculées.

Autres critères de couverture pour les expressions booléennes

Les diUérents critères de couverture de code présentés précédemment ne sont pas toujours ceux
qui sont utilisés. D’autres critères de couverture de code peuvent être proposés.
Le critère MC/DC fait débat entre ceux qui l’adoptent et ceux qui le rejettent, ainsi que ceux qui ne le comprennent pas. Et il n’y a pas vraiment de consensus au sein de ceux qui l’adoptent, puisqu’il en existe plusieurs versions.
Néanmoins, nous pouvons voir le critère MC/DC comme un compromis permettant d’une part de ne pas faire les tests exhaustifs (critère MCC), et d’autre part de ne pas se contenter de faire le minimum de tests (par exemple deux tests, où toutes les conditions sont à true pour l’un, et false pour l’autre).
Yu et al. [89] proposent une comparaison de diUérents critères de couverture de décisions. Xanthakis et al. [88] présentent et comparent diUérents critères de couverture de conditions et décisions.

Couverture faible des conditions/décisions modifiée (Weak MC/DC)

La couverture des conditions/décisions modiVée aUaiblie consiste à autoriser une condition à apparaître plusieurs fois dans une décision tout en permettant la satisfaction du critère MC/DC. Ainsi, une condition apparaissant plusieurs fois dans une décision n’est considérée qu’une seule fois.
Prenons par exemple un cas dégénéré : la décision (x && x) ne peut pas satisfaire le critère MC/DC puisqu’on ne pourra jamais faire varier la seconde branche du && tout en maintenant inchangée la première branche. Le critère MC/DC faible ne demande pas de montrer l’indépendance de la seconde branche car x apparaît ailleurs, endroit où son indépendance par rapport aux autres conditions (si elles existaient) serait montrée.
Dans le cas où plusieurs conditions sont apparemment les mêmes mais produisent des eUets de bord, cela se complique. Par exemple dans e && e, e pourrait être une lecture sur un Wux de données.
Dans ce cas, la raison d’utiliser un critère relâché n’est plus vraiment pertinent.

Couverture des conditions/décisions renforcée (RC/DC)

RC/DC est un critère proposé par Vilkomir et Bowen [83]. Ce critère se veut renforcer le critère MC/DC en ajoutant des contraintes de tests « dans la mesure du possible ».
Voici comment ils formulent la déVnition du critère RC/DC, avec en gras italique les parties qui diUèrent de la déVnition de MC/DC :  Avec MC/DC, si deux ensembles v1 et v2 de n conditions montrent l’indépendance de la condition i, alors (80 j < n; (j , i )v1[j] = v2[j]))^(v1[i] , v2[i]) et si d1 et d2 sont les décisions correspondant respectivement aux conditions v1 et v2, alors d1 , d2.
Pour RC/DC, dans la mesure du possible, on veut qu’il y ait une mesure supplémentaire par rapport à MC/DC montrant qu’avec les ensembles v1 et v2 on obtient d1 = d2.

Table des matières

I Introduction 
Objectifs de cette thèse
Contributions de cette thèse
Plan du manuscrit
II Développement de logiciels critiques et tests de couverture structurelle 
II.1 Criticité et sûreté des applications logicielles
II.1.1 Développement d’un logiciel critique
II.2 CertiVcations, tests et preuves formelles
II.2.1 Activités de tests
II.2.2 CertiVcats et preuves
II.3 Normes ou guides de développement de logiciels critiques
II.3.1 L’avionique civile en tant que domaine critique
II.3.2 Normes pour d’autres domaines critiques
II.4 Cycle de vie d’un logiciel et processus de développement
II.4.1 La vie d’un logiciel
II.4.2 Agencement de la vie d’un logiciel
II.4.3 L’importance du processus de développement pour un logiciel critique
II.5 Documentation et traçabilité pour les logiciels critiques
II.6 Processus de certiVcation (ou de qualiVcation)
II.7 Activités de tests
II.8 Évolution des activités de tests
II.8.1 Évolution des coûts
II.8.2 Évolution des techniques
II.9 Couverture de code
II.9.1 Objectifs
II.9.2 Outils pour la couverture de code
II.9.3 Un exemple de couverture de code
II.10 Conclusion du chapitre
III Le Langage mCaml et la couverture structurelle des expressions 
III.1 Le langage mCaml
III.1.1 Grammaire informelle des expressions du langage mCaml
III.1.2 Sémantique opérationnelle du langage mCaml
III.1.3 Arbre d’évaluation
III.2 SpéciVcation de la couverture des expressions pour mCaml
III.2.1 Règles formelles de couverture des expressions pour mCaml
III.2.2 Taux de couverture
III.3 Conclusion du chapitre
IV Couverture des conditions et des décisions pour mCaml 
IV.1 Critères de couverture pour les expressions booléennes
IV.1.1 Couverture des conditions (CC)
IV.1.2 Couverture des décisions (DC)
IV.1.3 Couverture des conditions/décisions (C/DC)
IV.1.4 Couverture des conditions multiples (MCC)
IV.1.5 Couverture des conditions/décisions modiVée (MC/DC)
IV.1.6 Autres critères de couverture pour les expressions booléennes
IV.2 Conditions et décisions pour mCaml : quatre sémantiques formelles
IV.2.1 Notations
IV.2.2 Sémantique 1 : repérage syntaxique aux branchements conditionnels
IV.2.3 Sémantique 2 : sémantique intermédiaire, généralisation aux opérateurs booléens
IV.2.4 Sémantique 3 : une extension de la sémantique 2, généralisation aux applications à retour booléen
IV.2.5 Sémantique 4 : généralisation aux expressions booléennes
IV.3 Choix de la sémantique
IV.4 Fonction de comptage des conditions d’une expression
IV.5 Conclusion du chapitre
V Couverture de code structurelle intrusive pour mCaml 87
V.1 Instrumentation de code mCaml pour la couverture des expressions
V.1.1 Instrumentation la plus générale
V.1.2 Instrumentation simple
V.1.3 Instrumentation avancée pour la couverture structurelle
V.1.4 Sémantique opérationnelle préservée
V.2 Instrumentation de code mCaml pour la mesure de satisfaction du critère MC/DC
V.3 Conclusion du chapitre
VI Couverture de code structurelle non-intrusive pour mCaml 
VI.1 Instrumentation pour la couverture structurelle simple
VI.1.1 Informations de mise au point produites par ocamldebug
VI.1.2 Génération des marques pour la couverture simple des expressions du langage mCaml
VI.2 Instrumentation pour les mesures des conditions et décisions
VI.2.1 Instrumentation de l’environnement d’exécution pour la mesure MC/DC
VI.2.2 Production de rapports de couverture avec la mesure MC/DC
VI.3 Conservation de la sémantique opérationnelle
VI.4 Conclusion du chapitre
VII Comparaison entre les approches intrusive et non-intrusive 
VII.1 Comparaison sémantique des deux techniques
VII.1.1 Équivalence des résultats produits par les deux techniques en l’absence de traitement particulier des appels terminaux
VII.1.2 Une diUérence notable des deux approches : les appels terminaux
VII.2 Comparaison pratique des approches intrusive et non intrusive
VII.2.1 Du point de vue de l’utilisateur
VII.2.2 Avantages et inconvénients
VII.3 MLcov : couverture structurelle par instrumentation du code source
VII.3.1 Caractéristiques générales de l’outil MLcov
VII.3.2 Sémantique utilisée par MLcov
VII.3.3 Un exemple de rapport de couverture avec MLcov
VII.4 Zamcov : couverture structurelle non intrusive
VII.4.1 Génération des informations de couverture
VII.4.2 Illustration
VII.5 Conclusion du chapitre
VIII Conclusion et Perspectives
Bibliographie

Télécharger le rapport complet