Analyse statique de logiciels temps-réel asynchrones embarqués – AstréeA

Le projet AstréeA concerne le développement de méthodes d'analyse statique par interprétation abstraite dans le but de vérifier la sûreté de fonctionnement de logiciels embarqués critiques asynchrones de grande taille.

La sûreté de fonctionnement des logiciels embarqués critiques, tels que ceux trouvés dans l'industrie aéronautique, ferroviaire, automobile ou médicale, est d'une importance capitale car toute erreur peut avoir des conséquences économiques ou humaines dramatiques.

La méthode de validation essentiellement utilisée est le test qui, malheureusement, voit son coût devenir prohibitif face à la complexité croissante des systèmes embarqués. Par conséquent, les tests ne couvrent généralement qu'une petite partie des cas d'exécution possibles, et certaines erreurs ne sont alors jamais découvertes pendant la validation. Cette situation est particulièrement préoccupante dans le cas des logiciels asynchrones, c'est à dire composés de plusieurs processus exécutés en parallèle, car le test ne permet de tester qu'une infime partie du très grand nombre d'ordonnancements de processus, alors que certaines erreurs ne se manifestent que pour certaines séquences d'exécution bien précises, difficiles à reproduire.

Les méthodes formelles offrent, au contraire, l'espoir d'une validation d'une rigueur mathématique. L'analyse statique par interprétation abstraite semble particulièrement bien adaptée à un contexte de validation industrielle puisqu'elle est automatique (sans interaction avec l'utilisateur), fonctionne directement sur le code source (et non sur un modèle simplifié), est sûre (exhaustive vis à vis de la sémantique formelle du langage donc sans faux négatif), et efficace. En contrepartie, elle peut souffrir de fausses alarmes (ou faux positifs), ce qui est le cas de la plus part des analyseurs statiques commerciaux.

L'expérience d'Astrée (http://www.astree.ens.fr/) a montré qu'il était possible de créer un analyseur statique atteignant zéro alarme, donc équivalent à une preuve de correction, en se concentrant sur un type de propriétés et de logiciels particuliers: dans ce cas précis, les erreurs à l'exécution dans du code avionique de contrôle/commande synchrone. Astrée est maintenant commercialisé et utilisé dans un contexte industriel.

Dans le projet AstréeA, nous nous intéressons au problème, plus difficile, des erreurs à l'exécution dans des logiciels asynchrones, en développant un prototype AstréeA basé sur Astrée. Suivant la démarche d'Astrée, AstréeA est spécialisé pour l'analyse des erreurs à l'exécution de logiciels asynchrones avioniques de grande taille fonctionnant sous un système d'exploitation temps-réel, Airbus fournissant un exemple typique de tel logiciel de taille industrielle (1.6 M de lignes).

La première phase du développement de l'analyseur AstréeA, soutenue par l'ANR, a permis de développer un modèle concret puis abstrait du système d'exploitation ARINC 653 et de son ordonnanceur, et un premier prototype d'analyseur qui, au bout de 4 années, s'est montré capable d'analyser le logiciel complet, avec il est vrai de nombreuses fausses alarmes.

L'essence de la proposition AstréeA est la continuation de cet effort, suivant le modèle qui a fait le succès d'Astrée: le raffinement incrémental de l'analyseur jusqu'à l'élimination de toutes les fausses alarmes. Pour AstréeA, ce raffinement concerne: (1) l'abstraction des interactions entre processus (abstractions relationnelles et sensibles à l'histoire des calculs), (2) le modèle de l'ordonnanceur (support pour de nouvelles primitives de synchronisation et prise en compte des priorités), (3) le modèle mémoire (prise en compte des variables volatiles), (4) les structures de données dynamiques (listes chaînées). Ces améliorations permettraient d'atteindre un niveau de précision élevé, éventuellement l'objectif de zéro alarme, et rendre possible une utilisation industrielle de l'analyseur AstréeA.