Sûreté de fonctionnement des logiciels aérospatiaux

Selon Leveson, la sûreté d'un logiciel implique d'assurer qu'il s'exécutera sans induire de risque non acceptable. La qualité de risque acceptable ou inacceptable doit être définie pour chaque système et implique souvent des décisions politiques, économiques et morales. Comme pour la sûreté matérielle, la sûreté logiciel est mise en place en identifiant les dangers potentiels tôt dans le processus de développement et en établissant des contraintes et modèles afin d'éliminer ou de contrôler ces dangers. Un logiciel critique est un logiciel qui contient des fonctions critiques[1].

L'aérospatiale est une discipline scientifique qui rassemble les techniques de l'aéronautique et de l'astronautique[note 1].

Une des principales motivations des applications logiciel, notamment pour les vols commerciaux, est d'optimiser les ressources dans un but économique. Cette optimisation peut être effectuée dans plusieurs catégories[2] :

• La réduction du poids des éléments permet d'économiser le fioul ;
• La consommation électrique doit être réduite au maximum pour éviter d'avoir à transporter trop de batteries ;
• L'utilisation d'outils comme la mémoire cache doit être limitée au maximum car elle entraîne un surcoût sur les processeurs qui sont extrêmement nombreux au sein d'un avion commercial.

La maintenance est également une grande source de coûts, c'est pourquoi les avions militaires sont utilisés pendant plusieurs décennies. Il est donc crucial d'apporter au sein des logiciels fiabilité, stabilité et facilité de maintenance[3].

Les modules doivent être au maximum réutilisables. Selon McDermid, une ligne de code vérifiée coûte entre 150 et 250 dollars. Le développement d'un logiciel de haut niveau de sûreté d'environ cent mille lignes de codes coûterait en moyenne 25 millions de dollars[4].

La sûreté des logiciels permet avant tout d'éviter les accidents qui représentent des coûts financiers et matériels importants comme le montre le tableau suivant[5]:

Évolution du nombre de lignes de code par projet aerospatial (en milliers)[6]

L'implication des logiciels dans l'aérospatiale augmente très rapidement. À titre d'exemple, les sondes Voyager, en 1977, contenaient 5 000 lignes de code informatique, tandis que l'ISS[note 2] en contient 1,4 million[7]. La défaillance de tels systèmes critiques peut avoir des conséquences graves comme des pertes de propriétés, des dégâts environnementaux, des blessures ou des décès[8].

La NASA par exemple impose sur ses logiciels une chance de défaillance de 10^-9 pour 10 heures de vol[9]. Dans plusieurs pays, une validation formelle et une démonstration de la sûreté de systèmes informatiques critiques pour la sécurité sont requis par les autorités de licences officielles[10].

Les logiciels de l'aérospatiale doivent assurer :

• la sûreté de fonctionnement ;
• l'efficacité ;
• une gestion en temps réel sûre ou un ratio coût/performance faible.

Depuis 1945, le nombre de morts par an pour 100 millions de milles parcouru par des passagers sur des vols commerciaux, hors actes de malveillance intentionnelle, est passé de 5 à moins de 0,05[11]. En plus de la sécurité liée au fonctionnement des logiciels, les méthodes et les organisations des projets doivent imposer une grande rigueur pour éviter au maximum les retards, qui impliquent également de forts surcoûts[7].

L'approche la plus souvent utilisée pour développer de larges systèmes aérospatiaux impliquant une équipe importante est de créer des systèmes embarqués sous forme d'intergiciels. Cela permet de déplacer la complexité bas niveau hors des applications qui interagiront avec ces systèmes, ainsi que de travailler avec de nombreux systèmes hétérogènes, de porter le code et de faciliter la maintenance[14].

Les systèmes embarqués ne permettent pas, contrairement aux ordinateurs classiques, de séparer le matériel du logiciel. Il est en effet compliqué d'abstraire le matériel pour pouvoir poser n'importe quelle couche logiciel dessus. Cela implique de plus grands coûts liés à la non réutilisabilité et à la double compétence éléctronicien/informaticien nécessaire[15].

Les données persistantes doivent être légères étant donné que la mémoire de stockage est souvent limitée et alimentée par des batteries. Il faut également gérer des interruptions électriques momentanées en conservant les informations[16].

Les processeurs multi-cœur posent plusieurs problèmes. Tout d'abord ils présentent une plus grande complexité de configuration et des fonctionnalités clés comme la mémoire cache et la gestion de pipelines. Mais le plus contraignant est la propriété non déterministe de l’ordre d'exécution des tâches qui est un challenge particulier pour construire des démonstrations sûres de système logiciel[2].

De nombreuses connexions existent au sein de ces systèmes complexes. Il faut donc une gestion appropriée des tâches parallèles. Cela implique qu'il faut garantir qu'un processus sera terminé avant une limite de temps et une limite de ressources dans le cadre d'applications aussi critiques[17].

Le respect de la vitesse d'exécution limite la complexité des algorithmes utilisés au sein de systèmes embarqués. À cela s'ajoute souvent le besoin de pouvoir surveiller l'activité des dis algorithmes, ajoutant encore de la complexité[18].

Les éléments embarqués au sein d'un appareil doivent assurer leur fonctionnalité tout en étant limités par la puissance fournie par le générateur. C'est particulièrement le cas pour les plus petits véhicules où la quantité d'énergie disponible est extrêmement limitée[19].

Pour économiser un maximum d'énergie, les algorithmes sont pensés en fonction de leur simplicité et de leur consommation. L'énergie utilisée par les systèmes informatiques embarqués peut représenter jusqu'à 20 % de la consommation totale[19].

Passagers décédés par an pour 160 millions de km, sur les vols commerciaux, hors actes de malveillance intentionnelleBernard 2009, p. 9

Tout avion qui décolle d'un aéroport doit répondre à des exigences nationales, voire internationales pour garantir l'intégrité des personnes à bord et autour de l'appareil[20]. De nombreuses organisations de certification et de réglementation aéronautique civile existent. Les deux principales sont[21] :

• l'AESA[note 4], créée en 2003 (voir exigences AESA) ;
• la FAA [note 3] aux États-Unis, créée en 1958 (Plus d'informations).

Ces deux agences définissent, entre autres, les exigences concernant la conception des avions, leur exploitation commerciale et les licences de pilotage. Les principales exigences applicables à la sureté de fonctionnement des systèmes sont définies dans le paragraphe numéroté 1309 à la fois dans le document CS-25 de l'AESA et le FAR-25 de la FAA[21]. Ils décrivent les exigences et sont généralement complétés d'annexes décrivant les moyens acceptés pour répondre à ces exigences[note 5].

Pour contrôler les pannes, les constructeurs d'engins aérospatiaux utilisent la redondance parallèle des systèmes. Tous les systèmes critiques sont multipliés (Au moins par 2). Ainsi si l'un des éléments tombe en panne, son identique parallèle est toujours disponible. Il existe 3 types de redondance[22] :

• Redondance de la surface (Surface redundancy) : Le matériel est dupliqué ainsi que son contrôleur ;
• Redondance du contrôleur : Le même matériel est contrôlé par deux contrôleurs ;
• Contrôleur avec redondance interne : un seul contrôleur gère le matériel, la sécurité par redondance est gérée par le contrôleur.

Cette redondance permet d'augmenter le temps avant la panne d'un élément. Par exemple si un élément a un taux de pannes de 3 × 10⁻⁵ par heure, alors si on le duplique en 3 exemplaires on obtient un taux de pannes de 3 × 10⁻⁵ × 3 × 10⁻⁵ × 3 × 10⁻⁵ = 9 × 10⁻¹⁵ par heure. On peut donc espérer que l'élément ne tombe en panne qu'après 1,1 × 10¹⁵ heures[23].

Le problème de cette méthode est que si un élément provoque des erreurs de calcul ou de mesure, le système ne saura pas définir quel élément a "raison". Pour pallier cela, il faudra utiliser des systèmes plus complexes comme la Triple redondance modulaire.

La redondance triple modulaire est une variante de la redondance N modulaire et est couramment utilisée dans les systèmes automatisés à tolérance de pannes. Un système de redondance N modulaire exécute successivement plusieurs tâches indépendantes. Chaque tâche distincte est exécutée par un nombre impair N de processeurs distincts. L'unité de vote obtient le résultat sans défaut pour la tâche en sélectionnant le résultat calculé par la majorité au moins (N + 1) / 2 des processeurs[24].

Pour un système de redondance triple modulaire, l'application de contrôle est reproduite sur un groupe de trois machines distinctes. Chaque tâche doit recevoir une entrée identique et est ensuite exécutée par les trois machines. Les résultats obtenus sont ensuite comparés, et le résultat calculé par la majorité des trois serveurs d'applications est utilisé comme le résultat final.

Dans une telle configuration, le système peut tolérer une machine défectueuse et toujours être en mesure de progresser. Si deux ou plusieurs machines sont détectées défectueuses, le système ne peut pas fonctionner de façon à tolérer des pannes. Afin de surmonter l'unique point de défaillance d'une unité centralisée de vote dans la redondance triple modulaire, le système réplique cette fonctionnalité sur chacune des machines[25].

La redondance triple modulaire est utilisée pour atténuer le taux d'erreurs dans un système FPGA[note 6] - [26].

Le développement basé sur le modèle utilise des composants de haut niveau, réutilisables et spécifiques au domaine. Cette méthode peut être utilisée à plusieurs niveaux, de la génération de fichiers de configuration à la génération de systèmes logiciels quasi complets[2].

SCADE, de la société Esterel, est un environnement intégré pour le développement basé sur le modèle et la vérification synchrone. L'exécution d'un logiciel doit être explicitée sous la forme de série d'étapes. À chaque étape[28] :

• Les données d'entrée sont lues ;
• Les données de sortie sont calculées ;
• Ces données de sortie sont écrites.

SCADE dispose d'un validateur de modèle intégré qui permet de vérifier les modèles directement en environnement de développement[29].

Les méthodes de spécifications traditionnelles ainsi que les techniques d'analyse de risque ajoutent la sûreté et la vérification en fin de développement. Au contraire, le développement orienté sureté a pour but d'intégrer les problématiques de sûreté dès le début de la conception logiciel[30] - [31].

La méthode STPA [note 9] a pour objectif d'identifier les instances de contrôle inadequates qui pourraient être dangereuses et les contraintes relatives à la sûreté nécessaires pour assurer un niveau de risque acceptable[32].

STAMP[note 10] est un modèle de causalité d'accident. Ce modèle part du principe que la sûreté est un problème de contrôle, c'est-à-dire que toute panne de composant, perturbation extérieur ou dysfonctionnement d'interaction entre systèmes est due à un mauvais contrôle de ces éléments. L'objectif est que le système continue à agir de manière sûre au fur et à mesure que les changements et adaptations ont lieu[33].

La méthode agile s'oppose à la méthode en cascade[note 11] qui consiste à diviser le processus de développement en étapes et de respecter leur ordre, à sens unique, sans retour en arrière[27]. La méthode agile est encore très peu présente dans le domaine de l'aerospatiale étant donné qu'elle présente certaines problématiques pour respecter la norme DO-178B[34]:

• La difficulté à s'adapter aux très gros projets ;
• Il est difficile d'augmenter la fréquence des relations avec les sous-traitants ;
• Des portions de codes héritées d'anciens projets font souvent partie des spécifications.

D'autres méthodes apparaissent dans le cadre de recherches, parfois en collaboration avec des entreprises pour des projets réels. C'est le cas par exemple de la Formalisation et validation d'exigences critiques de sûreté[35]

La technique du Health Management[note 12] est déjà largement utilisée pour les équipements mécaniques ainsi que les systèmes électroniques. Elle permet d'améliorer leur robustesse et de réduire les coûts. De ce fonctionnement commence donc à apparaître le Software Health Management[note 13] (SHM), dont le concept est utilisé dans les logiciels de tests de l'aerospatiale[36].

Une grande partie de l'effort de sûreté va dans la tentative de preuve que les modèles existants sont sûrs plutôt que de construire des modèles sûr depuis leur conception. Le seul espoir pour la conception sûre, pratique et rentable est de concevoir des systèmes de sécurité dès la base de la conception[38].

En conception axée sur la sécurité[note 15], les informations nécessaires aux concepteurs pour prendre de bonnes décisions sont mises à leur disposition avant la conception et l'analyse est effectuée en parallèle au processus de conception plutôt qu'après. Une telle approche de conception sera non seulement beaucoup moins chère, mais entraînera la création de systèmes beaucoup plus sûrs[38].

Parce que la première cause des accidents dans les anciens systèmes est la défaillance de composants, l'analyse des risques des techniques de conception de sécurité était portée sur l'identification des composants critiques et/ou la prévention de leur arrêt (augmentant ainsi l'intégrité des composants) ou de fournir la redondance pour atténuer les effets de la défaillance d'un composant. Souvent, aucune analyse spéciale (analyse de risque ou de sécurité) n'est appliquée au logiciel[30].

La première étape pour mettre en œuvre la sûreté est de séparer les échecs en deux parties[39] :

• échecs impactant la sûreté ;
• échecs n'impactant pas la sûreté.

SFTA[note 16] qui est une méthode d'analyse de la sûreté de la conception des logiciels est utilisée pour s'assurer que la logique contenue dans la conception logicielle n'entraînera pas de fautes de sûreté et aussi pour déterminer les conditions environnementales qui pourraient amener le logiciel à causer des fautes de sûreté dans le système[39].

Assurer que de tels logiciels critiques ne plantent pas est fait en procédant à des tests[12].La définition des tests sur des logiciels est donnée par Miller "Le but général des tests est d'affirmer la qualité des logiciels en exécutant le logiciel de façon systématique dans des circonstances prudemment contrôlées[40].

Le processus d'automatisation des tests est une étape importante dans la réduction des coûts de développement des logiciels et de leur maintenance[40].

MBT[note 17] est une approche dont le but est de produire des systèmes logiciels de test se basant sur un modèle formel à partir duquel les cas de tests sont générés. Pour les tests dans l'aérospatiale, des méthodes particulières du MBT sont utilisées. On a par exemple le TTF (Test Template Framework) qui est utilisé par Fatest pour générer des tests unitaires. Notons que ces tests unitaires (produits par Fatest) ne sont pas les plus utilisés dans le domaine du MBT[41].

L'idée derrière la TTF, ainsi que d'autres méthodes MBT est d'analyser une spécification Z dérivée de cas de tests abstraits, c'est-à-dire des cas de test écrit en Z qui sont par la suite utilisés pour tester la mise en œuvre correspondante. Chaque classe de test est un schéma Z spécifiant une condition de test[42].

Depuis que la TTF a plusieurs différences avec les autres MBT méthodes, il est nécessaire d'expliquer comment il se comporte avec les oracles de test. Un oracle de test est un moyen par lequel il est possible de déterminer si un cas de test a trouvé une erreur dans sa mise en œuvre ou non. Dans TTF, la spécification agit comme un oracle de test. En effet, selon le fonctionnement de la TTF[43]:

• les cas de test abstraits doivent être affinés en cas de tests exécutables ;
• ces cas de test sont exécutés par le programme sous essai ;
• la sortie produite par le programme pour un cas de test est abstraite au niveau de la spécification (si cela est possible) ;
• à la fois le cas de test abstrait et sa sortie abstraite correspondante sont substitués dans le schéma de l'opération de Z appropriée.

De cette manière, le prédicat de l'opération devient un prédicat constant qui vaudra vrai ou faux[43].

La Black box testing est référencée comme un test fonctionnel parce qu'il se concentre sur les sorties du programme (à tester), sorties générées par des certaines données en entrée et certaines conditions d'exécution. Avec cette méthode, le testeur du programme n'a pas besoin d'avoir accès au code source du produit. En se basant sur les exigences du produit le testeur sait à quel comportement s'attendre de la black box[40]. Seuls les exigences sont utilisées pour implémenter les cas de test[40].

La méthode White-box testingest référencée comme étant un test structurel parce qu'il prend en compte la structure interne du système [44]. Pendant un test White box, le testeur est conscient de la structure interne du logiciel et implémente les cas de test en exécutant différentes méthodes et en leur passant des paramètres spécifiques[44].

D'autres méthodes de test comme existent. On a par exemple la Grey Box testing qui est une combinaison de la White et de la Black box testing[44].

Les tests sont critiqués parce qu'ils sont chers (pour des systèmes complexes) et finalement ne peuvent pas vraiment prouver qu'il n'y a pas de fautes dans de tels systèmess[12] - [40]. C'est pourquoi certaines infrastructures se tournent vers les méthodes formelles [12].

Une méthode est dite formelle si elle est composée d'une notation formelle ainsi que d'une analyse technique. De plus elle ne doit pas être ambiguë et avoir une syntaxe et une sémantique définies mathématiquement[45].

L'objectif d'utiliser des méthodes formelles est de pouvoir échanger des informations précises entre plusireurs interlocuteurs, sans risque de mauvaise compréhension ou d'interprétation[46].

Les méthodes formelles n'ont pas pour but de remplacer les tests mais de les compléter et les automatiser. À partir des spécifications formelles, il est possible de générer automatiquement le code des scénarios de test. Ainsi les tests sont plus rapides à mettre en place et assurent qu'ils vérifient bien les exigences du logiciel[47].