Accueil🇫🇷Chercher

Sûreté de fonctionnement des logiciels aérospatiaux

La sûreté de fonctionnement des logiciels aérospatiaux correspond à la mesure du risque d'un logiciel ou d'une partie de logiciel, souvent critique, impliqué dans le fonctionnement d'un engin aéronautique ou astronautique.

Les principales motivations sont économiques et techniques. Il est important dans ces domaines impliquant autant d'argent d'éviter les pertes, que ce soit matériel ou humain, entraînant des surcoûts énormes. Les difficultés à gérer sont multiples, il faut créer une grande quantité de systèmes embarqués, gérer des données persistantes légères, valider des exécutions par processeurs multi-cœurs, répondre à des problématiques temps-réel, limiter la consommation d'énergie et répondre à des contraintes de développement strictes.

Il existe des architectures spécifiques à la sûreté de fonctionnement basé sur la redondance matérielle ou logicielle. Les méthodes employées importent également pour limiter les coûts de retard ou de mauvais fonctionnement, mais doivent en plus apporter la sûreté en parallèle du bon fonctionnement. D'abord en amont, pendant la conception, sont utilisées des méthodes comme l'architecture basée sur le modèle, le développement orienté sûreté ou l'utilisation de la méthode agile dans l'aérospatiale. Mais également en fin de processus, où les programmes sont vérifiés via la vérification automatique ou encore les tests unitaires

Définitions

Sûreté de fonctionnement

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].

Aérospatiale

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

Objectifs

Économiques

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]:

SystèmeCoûtDescription de la perte
Ariane 5 (1996)594 millions de dollarsErreur logiciel impliquant une perte de contrôle.
Delta III (1998)336 millions de dollarsErreur logiciel causant une perte de contrôle et l'auto-destruction.
Titan 4B (1999)1.5 milliard de dollarsLa mauvais placement d'une décimale dans un logiciel de vol a causé le déploiement prématuré de charges dans une orbite trop basse.
Mars Climate Oribiter (1999)524 millions de dollarsUne erreur d'unité métrique dans un logiciel d’atterrissage a causé une mauvaise trajectoire et la destruction pendant l'entrée dans l'atmosphère martienne.
Zenit 3SL (2000)367 millions de dollarsUne erreur logiciel a prématurément éteint une fonctionnalité, empêchant le satellite d'atteindre son orbite.

Techniques

É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].

Coûts et retards pour les programmes de modernisation de la FAA [note 3]
Projet Coût total du programme

(en million de $)

Date d'opération
Estimation originale Coût réel Estimation originale Date réelle
WAAS 892.4 2900.0 1998 2000
STARS 940.2 1400.0 1998 2002
AMASS 59.8 151.8 1996 2002

Challenges

Les logiciels critiques (comme ceux des zones industrielles, de l'industrie de l'automobile, et les applications de l'aérospatiale) ne devraient jamais planter [12].

Les systèmes électroniques pour les véhicules modernes doivent être conçus pour respecter des exigences strictes en matière de performances temps-réel, de sûreté, de consommation d'énergie et de sécurité[13].

Systèmes embarqués

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].

Gestion des données persistantes

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].

Processeurs multi-cœur

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].

Temps réel

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].

Consommation d'énergie

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].

Exigences

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] :

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].

Architectures pour la sûreté des logiciels

Systèmes à redondance parallèle

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−5 par heure, alors si on le duplique en 3 exemplaires on obtient un taux de pannes de 3 × 10−5 × 3 × 10−5 × 3 × 10−5 = 9 × 10−15 par heure. On peut donc espérer que l'élément ne tombe en panne qu'après 1,1 × 1015 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.

Redondance Triple 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].

Méthodes de développement

Les méthodes de développement dans l'aerospatiale doivent se soumettre aux normes de sécurités applicables aux logiciels critiques de l'avionique. Elles doivent donc respecter les conditions énoncées dans le DO-178C[27].

Architecture ou développement dirigé par le modèle[note 7] - [note 8]

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].

Développement orienté sureté (Safety Driven Design)

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].

Méthode Agile pour l'aerospatiale

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.

Autres méthodes

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].

Analyse et vérification formelle

La vérification et la validation représentent plus de 50 % des coûts de développement de logiciels. Leur importance est capitale en sachant que plus une erreur est détéctée tardivement, plus sa correction sera couteuse[37].

Vérification automatisée[note 14]

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].

Tests unitaires

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].

Model-Based Testing

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

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 White Box Testing

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].

Méthodes et langages formels

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].

Références

  1. Leveson 1986, p. 139
  2. Sharp 2010, p. 623
  3. Sharp 2010, p. 625
  4. Habli 2007, p. 193
  5. Bell 2008
  6. Bell 2008, p. 135
  7. Hayhurst 2001, p. 7
  8. Leveson 1986, p. 125
  9. Leveson 1986, p. 126
  10. Leveson 1986, p. 135
  11. Bernard 2009, p. 9
  12. Bruno 2003, p. 196
  13. Abdallah 2010, p. 584
  14. Sharp 2010, p. 622
  15. Henzinger 2006, p. 1-2
  16. Roll 2003, p. 79
  17. Roll 2003, p. 80
  18. Odavic 2010, p. 3044
  19. Spinka 2011, p. 83
  20. Bernard 2009, p. 15
  21. Bernard 2009, p. 16
  22. Bennett 2010, p. 1
  23. Nanda 2009, p. 67
  24. Fuhrman 1995, p. 75
  25. Fuhrman 1995, p. 77
  26. Allen 2011, p. 1
  27. VanderLees 2009, p. 6.D.3-1
  28. Martin 2013, p. 6
  29. Martin 2013, p. 8
  30. Stringfellow 2010, p. 515
  31. Owens, p. 1
  32. Stringfellow 2010, p. 518
  33. Owens, p. 4
  34. VanderLees 2009, p. 6.D.3-10
  35. Cimatti 2008, p. 68
  36. Xie 2013, p. 1928
  37. Wiels2012 2012, p. 2
  38. Stringfellow 2010, p. 516
  39. Leveson 206, p. 515
  40. Latiu 2012, p. 1
  41. Cristia 2011, p. 128
  42. Cristia 2011, p. 129
  43. Cristia 2011, p. 130
  44. Latiu 2012, p. 2
  45. Wiels 2012, p. 2
  46. Bernard 2009, p. 10
  47. Wiels 2012, p. 6

Notes

  1. « Larousse.fr : encyclopédie et dictionnaires gratuits en ligne », sur larousse.fr (consulté le ).
  2. International Space Station
  3. Federal Aviation Administration
  4. Agence Européenne de la Sécurité Aérienne
  5. Acceptable Means of Compliance (AMC)
  6. "field-programmable gate array" en français "circuit logique programmable"
  7. Model Driven Architecture
  8. Model Based Development
  9. Systems Theoretic Process Analysis
  10. System-Theoretic Accident Modeling and Process
  11. waterfall method
  12. En français "Management par la santé"
  13. En français "Management de logiciel par la santé"
  14. Automated verification
  15. Safety-driven Design
  16. SOFTWARE FAULT TREE ANALYSIS
  17. Model-Based Testing

Bibliographie

  • (en) David C. Sharp, « Challenges and Solutions for embedded and Networked Aerospace Software Systems », Proceedings of the IEEE, vol. 98, no 4, , p. 621-634 (ISSN 0018-9219, DOI 10.1109/JPROC.2009.2039631)
  • (en) W. Roll, « Towards model-based and CCM-based applications for real time systems », Proceedings of the IEEE, , p. 75-82 (ISBN 0-7695-1928-8, DOI 10.1109/ISORC.2003.1199238)
  • (en) Ahmed Abdallah, « Hardware/Software Codesign of Aerospace and Automotive Systems », Proceedings of the IEEE, vol. 98, no 4, , p. 584-602 (ISSN 0018-9219, DOI 10.1109/JPROC.2009.2036747)
  • (en) Hayhurst, K.J., « Challenges in software aspects of aerospace systems », Proceedings of the IEEE, , p. 7-13 (ISBN 0-7695-1456-1, DOI 10.1109/SEW.2001.992649)
  • (en) Nancy G. Leveson, « Software Safety: Why, What, and How », ACM Computing Surveys, vol. 18, no 2, , p. 125-163 (DOI 10.1145/7474.7528)
  • (en) Habli, « Challenges of Establishing a Software Product Line for an Aerospace Engine Monitoring System », IEEE, , p. 193-202 (ISBN 978-0-7695-2888-5, DOI 10.1109/SPLINE.2007.37)
  • (en) Martin L, « A Methodology for Model-based Development and Automated Verification of Software for Aerospace Systems », IEEE, , p. 1 - 19 (ISBN 978-1-4673-1812-9, ISSN 1095-323X, DOI 10.1109/AERO.2013.6496950)
  • (en) Stringfellow, « Safety-Driven Design for Software-Intensive Aerospace and Automotive Systems », Proceedings of the IEEE, vol. 98, no 4, , p. 515-525 (ISSN 0018-9219, DOI 10.1109/JPROC.2009.2039551)
  • (en) Owens, Herring, Dulac, Leveson, Ingham et Weiss, « Application of a Safety-Driven Design Methodology to an Outer Planet Exploration Mission », Proceedings of the IEEE, , p. 1-24 (ISBN 978-1-4244-1488-8, ISSN 1095-323X, DOI 10.1109/AERO.2008.4526677)
  • (en) David G. Bell, « Automated Software Verification & Validation: An Emerging Approach for Ground Operations », IEEE, , p. 1-8 (ISBN 978-1-4244-1488-8, ISSN 1095-323X, DOI 10.1109/AERO.2008.4526648)
  • (en) Allen, Edmonds, Swift, Carmichael, Chen Wei Tseng, Heldt, Anderson et Coe, « Single Event Test Methodologies and System Error Rate Analysis for Triple Modular Redundant Field Programmable Gate Arrays », IEEE, vol. 58, no 3, , p. 1040-1046 (ISSN 0018-9499, DOI 10.1109/TNS.2011.2105282)
  • (en) Alessandro Cimatti, Marco Reveri, Angelo Susi et Stefano Tonetta, « Formalization and Validation of Safety-Critical Requirements », EPTCS, , p. 68-75 (DOI 10.4204/EPTCS.20.7)
  • (en) Steven H. VanderLees, « Escape the waterfall: agile for aerospace », IEEE, , p. 6.D.3-1 - 6.D.3-16 (ISBN 978-1-4244-4078-8, DOI 10.1109/DASC.2009.5347438)
  • (en) Maximiliano Cristia, « Applying the Test Template Framework to Aerospace Software », IEEE, (lire en ligne)
  • (en) Loubach, « Testing Critical Software: A Case Study for an Aerospace Application », dans 25th Digital Avionics Systems Conference, (ISBN 1-4244-0378-2, DOI 10.1109/DASC.2006.313741)
  • (en) von Mayrhauser, « The Sleuth approach to aerospace software testing », Proceedings of the IEEE, vol. 2, , p. 61-75 (ISBN 0-7803-2473-0, DOI 10.1109/AERO.1995.468918)
  • (en) von Mayrhauser, « Testing applications using domain based testing and Sleuth », IEEE, vol. 2, , p. 206-215 (ISBN 0-8186-6665-X, DOI 10.1109/ISSRE.1994.341375)
  • (en) von Mayrhauser, « Domain based regression testing », IEEE, , p. 26-35 (ISBN 0-8186-6330-8, DOI 10.1109/ICSM.1994.336792)
  • (en) Weiqi Xie, « Study on The Application of Health Management Techniques in Aerospace Testing Software », IEEE, , p. 1928-1933 (ISBN 978-1-4799-1014-4, DOI 10.1109/QR2MSE.2013.6625956)
  • (en + fr) Romain Bernard, « Analyses de sûreté de fonctionnement multi-systèmes », IEEE, (lire en ligne)
  • (en) Spinka et Hanzalek, « Energy-Aware Navigation and Guidance Algorithms for Unmanned Aerial Vehicles », IEEE, vol. 2, , p. 83-88 (ISBN 978-1-4577-1118-3, ISSN 1533-2306, DOI 10.1109/RTCSA.2011.22)
  • (en) Bennett, Mecrow, Atkinson et Atkinson, « Failure mechanisms and design considerations for fault tolerant aerospace drives », IEEE, , p. 1-6 (ISBN 978-1-4244-4175-4, DOI 10.1109/ICELMACH.2010.5607981)
  • (en) Leveson, N.G. et Harvey, P.R., « Analyzing Software Safety », IEEE, , p. 569 - 579 (ISSN 0098-5589, DOI 10.1109/TSE.1983.235116)
  • (en) Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux et Xavier Rival, « A static analyzer for large safety-critical software », ACM Computing Surveys, , p. 196 - 207 (ISBN 1-58113-662-5, DOI 10.1145/780822.781153)
  • (en) Wiels, Delmas, Doose, Garoche, Cazin et Durrieu, « Formal Verification of Critical Aerospace Software », aerospacelab-journal, no 4, (lire en ligne)
  • (en) G. I. Latiu, O. A. Cret et L. Vacariu, « Emerging Intelligent Data and Web Technologies », Automatic Test Data Generation for Software Path Testing Using Evolutionary Algorithms, Bucharest, , p. 1-8 (ISBN 978-1-4673-1986-7, DOI 10.1109/EIDWT.2012.25)
  • (en) M. Nanda, « EA formal method approach to analyze the design of aircraft Flight Control Systems », IEEE, Vancouver, , p. 64-69 (ISBN 978-1-4244-3463-3, DOI 10.1109/SYSTEMS.2009.4815773)
  • (en) Thomas A. Henzinger et Joseph Sifakis, « The Embedded Systems Design Challenge », FM, , p. 1-15 (ISBN 978-3-540-37216-5, DOI 10.1007/11813040_1)
  • (en) Milijana Odavic, Mark Sumner, Pat Wheeler et Jing Li, « Real-Time Fault Diagnostics for a Permanent Magnet Synchronous Motor Drive for Aerospace Applications », IEEE, , p. 2044-3049 (ISBN 978-1-4244-5287-3, DOI 10.1109/ECCE.2010.5618381)
  • (en) Christopher Fuhrman, Sailesh Chutani et Henri Nussbaumer, « A Fault-Tolerant Implementation Using Multiple-Task Triple Modular Redundancy », IEEE, , p. 75-80 (ISBN 0780330595, DOI 10.1109/WFCS.1995.482652)
Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.