Langages Applicatifs et Machines Abstraites pour la Couverture de Code Structurelle

Criticité et sûreté des applications logicielles

Définitions
• Un système critique est un système dans lequel une panne peut avoir des conséquences dramatiques, tels des morts ou des blessés graves, des dommages matériels importants, ou des conséquences graves pour l’environnement ou l’économie.
• Un logiciel critique est un composant d’un système critique. Son dysfonctionnement mettrait en péril la sécurité de personnes ou aurait d’autres conséquences graves.
• On parle de sûreté de logiciels ou de logiciels sûrs quand on veut s’assurer qu’ils ne se comportent pas de manière non conforme aux attentes (e.g., arrêt intempestif, calculs erronés).
Remarque. La sécurité des logiciels se base sur l’étude de sa vulnérabilité et sa capacité à résister aux attaques. C’est un domaine qui n’est pas traité dans cette thèse et qu’il ne faut pas la confondre avec la sûreté des logiciels.

Développement d’un logiciel critique

Les développements de logiciels critiques suivent des pratiques plus contraignantes que ceux pour des logiciels non critiques, aVn d’obtenir le meilleur niveau de qualité et de sûreté. On rappelle qu’une défaillance d’un logiciel critique causant la mort de personnes pourrait avoir des coûts sans limite. L’avionique civile est le domaine qui impose les processus de développement les plus stricts et contraignants. Le ferroviaire possède des normes similaires avec toutefois un contexte de déploiement diUérent. Le guide DO-178B[73] donne probablement la plus connue des pratiques de développement de logiciels critiques actuellement, notamment du fait de sa rigueur. C’est un guide destiné au domaine des logiciels utilisés dans l’avionique civile. Un logiciel développé pour un avion à usage civil doit répondre aux exigences de ce document. La version DO-178C[74], publiée en décembre 2011, commence à remplacer la DO-178B. En eUet, d’une part la technologie évolue. On veut introduire de nouvelles techniques de développement de logiciels, mais aussi et surtout de vériVcation. D’autre part, les besoins évoluent aussi. On n’attend pas la même chose d’un avion aujourd’hui qu’on en attendait il y a vingt ans  .

Certifications, tests et preuves formelles 

Définition. Un certificat est un document qui atteste du suivi et du respect d’une certaine quantité d’exigences. Il peut être un contrôle de savoirs ou savoir-faire. Il peut être la déclaration de possession d’un bien matériel. Ou encore il peut attester du respect d’un processus de production. En général, un certiVcat doit être vériVable, en ce sens qu’il doit exister une démarche permettant de le vériVer.

À propos de la notion de « certiVcat »
Voici quelques exemples de certiVcats dans des contextes très diUérents.
– un certiVcat d’aptitude professionnelle (C.A.P.) ;
– un certiVcat d’immatriculation (ex-carte grise) ;
– un certiVcat d’agriculture biologique ;
– un certiVcat SSL/TLS (Secure Sockets Layer/Transport Layer Security).

Pour les logiciels critiques, un certiVcat est délivré pour un logiciel dont le développement a suivi un cahier des charges précis et rigoureux. Un certiVcat n’a alors de valeur que si le cahier des charges est pertinent et que l’autorité de certiVcation est de conVance et compétente. Parmi les quelques exemples de certiVcats d’autres domaines présentés plus haut, c’est le certiVcat d’agriculture biologique qui en est le plus analogue.

Activités de tests

Les activités de tests font partie de la plupart des processus de certiVcation des logiciels. Selon Myers [62], leur premier but est de trouver les erreurs, si bien qu’un ensemble de tests ne mettant aucune erreur en évidence est a priori considéré en échec. Il s’agit de vériVer que pour certaines entrées, on obtient bien les sorties attendues, mais surtout il s’agit de chercher et trouver les scénarios où les sorties attendues ne correspondent pas aux sorties obtenues. Ces activités permettront également de vériVer qu’on n’a pas écrit de code inatteignable. Leur second but est de montrer qu’on a bien envisagé tous les cas de Vgure et qu’on les a testés, pour ne pas avoir de mauvaise surprise lors de la mise en production. Si le développeur peut faire ses propres tests pour dénicher ses propres erreurs, au Vnal le testeur doit préférablement être une autre personne aVn de ne pas biaiser les tests. Le testeur vériVe ainsi le travail du développeur, donc la conformité de la production du développeur par rapport aux spéciVcations du cahier des charges. La plupart du temps, le testeur n’a pas accès au code produit par le développeur. Il doit produire ses tests d’après les spéciVcations, et non d’après le code du développeur. Le coût des activités de tests est grand par rapport au coût total du développement d’un logiciel. Mais il est généralement préférable de payer ce coût le plus tôt possible pour éviter les mauvaises surprises une fois le produit mis en production. Cependant, devant la part importante du coût du test, découle rapidement une volonté de réduire ce coût sans altérer la qualité du produit. De plus, les logiciels devenant de plus en plus complexes, que ce soit à cause de leurs tailles ou des fonctionnalités intrinsèques, les coûts de développement et de tests augmentent.

Certificats et preuves

Vis-à-vis de la sûreté de fonctionnement, un certiVcat n’est pas une preuve au sens mathématique ou formel du terme. Ainsi, un logiciel certiVé n’est généralement pas un logiciel dont le fonctionnement et l’implantation ont été entièrement prouvés mathématiquement. Cependant, une preuve mathématique peut être un certiVcat, en partie ou entièrement. En eUet, les avancées dans les méthodes formelles sont tout à fait intéressantes. Par exemple, le projet CompCert[51] propose un compilateur ciblant un assembleur PowerPC pour un grand sousensemble du langage C, dont la majeure spéciVcité est de fournir la preuve mathématique des différentes transformations de langage eUectuées par le compilateur. Cela signiVe que la propriété de conservation de la sémantique du programme, lors des traductions d’un langage à un autre langage, est prouvée. Sans aller jusqu’à une certiVcation totale d’un logiciel par la preuve, son utilisation partielle a été validée dans le domaine de l’avionique civile. Notamment, CAVEAT, un prouveur pour programmes écrits en langage C et développé au Commissariat à l’Énergie Atomique, a été utilisé dans le processus de vériVcation d’un logiciel critique destiné à l’avionique civile par Airbus [79]. Les preuves servent à montrer et à garantir des propriétés de sûreté. Cependant les tests ne pourront probablement jamais être remplacés entièrement par les preuves, car on veut s’assurer avec les tests que les spéciVcations sont bien implantées mais aussi qu’elles expriment eUectivement ce que leurs auteurs pensent qu’elles expriment. Ce sera nécessaire tant que les langues naturelles exprimeront des propos sujets à interprétation et interviendront dans la conception des logiciels. D’autre part, actuellement, il est techniquement plus facile de faire des tests que de faire des preuves dès que les programmes deviennent complexes. La phrase suivante de Donald Knuth illustre la situation de la preuve face au test : « Beware of the above code ; I have only proved it correct, not tried it. ».

Normes ou guides de développement de logiciels critiques

L’avionique civile en tant que domaine critique

Avant l’arrivée des logiciels critiques, il y avait de manière plus générale les systèmes critiques qui n’embarquaient pas de logiciels. Les premiers avions de ligne civils datent des environs de 1920. Ils permettaient de transporter une dizaine de personnes. Après la seconde guerre mondiale, sont apparus les avions de ligne transportant une centaine de personnes (e.g., Boeing 377). Aujourd’hui, les avions de ligne transportent jusqu’à plus de 800 passagers (e.g., Airbus A380) et surtout, ils embarquent des logiciels de plus en plus nombreux et complexes. Pour qu’un logiciel critique puisse être utilisé, il faut obtenir l’aval de l’autorité de régulation. Pour l’avionique civile, aux États-Unis, il s’agit de la Federal Aviation Administration (FAA) . Son homologue européen est l’Agence Européenne de la Sécurité Aérienne (AESA). Dans le contexte des systèmes critiques, ces agences sont chargées de promouvoir le plus haut niveau possible de sécurité pour les passagers. Ces agences exigent que les systèmes critiques soient conçus de la manière la plus sûre possible. Pour les logiciels, tout comme pour le matériel (au sens large, c’est-à-dire incluant le matériel mécanique et le matériel électronique), elles recommandent le suivi de normes ou de guides. Aux États-Unis, la Radio Technical Commission for Aeronautics (RTCA, Inc.)  est l’organisation chargée de développer des guides techniques pour les autorités gouvernementales et industrielles servant à l’avionique, et la FAA est son principal soutien. En 1980, la RTCA a formé un comité (SC-145) pour établir un guide pour le développement des logiciels destinés à l’avionique, c’est lui qui a produit le document « Software Considerations in Airborne Systems and Equipment CertiVcation », édité en janvier 1982 sous la référence DO-178 [46]. Un autre comité a été formé pour produire une première révision du document, ce qui a donné en 1985 la publication de la DO-178A [72]. En 1989, un nouveau comité a été formé pour travailler sur une nouvelle version aVn de traiter de nouvelles problématiques dont la qualiVcation des outils, ce qui a donné en 1992 la publication de la version la plus connue à ce jour qui est la DO-178B [73]. En décembre 2011, la DO-178C tant attendue arrive et complète la DO-178B en répondant à de nouvelles demandes dont l’introduction des « méthodes formelles » [74]. Celles-ci avaient cependant déjà été employées dans le cadre de développements DO-178B [80]. La nouvelle révision DO-178C remplacera peu à peu son prédécesseur DO-178B ; mais il faut du temps pour que la transition se fasse notamment en raison des projets qui ont démarré avant sa publication. Dans cette thèse, on fera par défaut référence à la version DO-178B. La plupart du temps, ce qui fait référence dans cette thèse à la DO-178B reste valide pour la DO-178C .

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 Conclusion

Télécharger le rapport complet