Vérification formelle de logiciels critiques aérospatiaux

Le logiciel embarqué implémente de plus en plus de fonctions dans le domaine aérospatial, et notamment des fonctions critiques. L’Ingénierie Dirigée par les Modèles a changé le cycle de vie des logiciels en introduisant des modèles dans les phases amont du développement. La vérification et la validation sont essentielles, sur les modèles et sur le  code, et sont essentiellement mises en œuvre par la simulation et le test. Cependant, les méthodes formelles, basées sur l’analyse mathématique du programme ou du modèle, sont en cours de transfert vers l’industrie pour la vérification de logiciel critique.
Cet article présente le contexte du développement logiciel aérospatial, donne un aperçu des méthodes formelles existantes et des pratiques industrielles dans ce domaine et décrit les travaux Onera sur la vérification formelle de logiciel critique au niveau modèle et au niveau code. Ces travaux concernent quatre thématiques :

• Méthodes et processus spécifiques pour le domaine aérospatial
• Ingénierie des modèles au niveau plateforme
• Coopération de techniques d’analyse
• Automatisation des tests à l’aide de méthodes formelles

Chacun de ces thèmes est un domaine de recherche ; il est donc impossible dans un seul article de fournir un état de l’art détaillé et une liste exhaustive des axes de recherche pour chacun. Cet article a plutôt pour objectif de donner une vision en largeur du domaine et de présenter les travaux Onera.