Analyse statique de logiciels asynchrones de contrôle-commande – THESEE

Projet THÉSÉE
Analyse statique de logiciels asynchrones de contrôle-commande

1) Introduction

Le projet se situe dans le contexte de la vérification de logiciel temps
réel embarqué critique pour lequel la preuve d'absence d'erreurs à
l'exécution, est une étape crutiale. À l'opposé des explorations non
exhaustives, les analyseurs statiques n'omettent jamais aucune erreur
possible. Pour ce faire, l'analyseur construit automatiquement un modèle
sémantique abstrait infini mais représentable en machine du programme. Il
calcule ensuite automatiquement, et en un temps fini, une sur-approximation
des états atteignables pour en déduire une sur-approximation des erreurs.
Le problème est alors celui des fausses alarmes (erreurs potentielles
signalées ne correspondant en réalité à aucune exécution possible). S'il
n'y a aucune alarme, l'analyse statique est une preuve formelle.

L'analyseur ASTRÉE (http://www.astree.ens.fr/) montre que l'analyse
statique peut être spécialisée pour des familles de programmes et aboutir à
des résultats et performances excellents. L'application à deux logiciels
avioniques synchrones critiques développés par Airbus démontre que
l'objectif de zéro fausse alarme peut être atteint sur de gros codes
synchrones (programmes séquentiels de quelques centaines de milliers de
lignes).

L'objectif du projet THÉSÉE est de considérer l'analyse statique de
programmes de contrôle/commande asynchrones (donc parallèles et
distribués). Ces programmes sont très difficiles à mettre au point car les
erreurs à l'exécution, qu'elles soient classiques (comme les débordements
arithmétiques ou d'indices de tableaux) ou liées à la concurrence (comme
les interblocages), sont excessivement difficiles à reproduire. L'analyse
statique est donc une alternative viable.

Mots clés:

Méthodes formelles (abstraction)
Processus et outils de vérification et validation (preuves)
Systèmes et applications embarqués innovants

2) Objectifs de recherche du projet

L'analyse de codes de contrôle/commande asynchrone présente un intérêt
économique évident pour les logiciels critiques. Les analyseurs
commerciaux existants sont trop imprécis pour servir à la vérification
formelle. L'analyseur ASTRÉE est exceptionnellement précis et performant
mais restreint aux codes synchrones.

Le projet THÉSÉE doit lever les verrous technologiques pour l'analyse de
ces codes asynchrones:

a) la définition de la sémantique des programmes parallèles de
contrôle/commande écrits en C exécutés dans le contexte de systèmes
d'exploitation temps-réel (comme POSIX, LynxOS, CsLEOS, TimeSys Linux,
etc).

b) l'abstraction du parallélisme (tenant compte des aspects multitâches,
processus légers avec priorité, niveaux d'interruptions, etc).

3) Objectifs industriels du projet

Les partenaires industriels du projet (Airbus, EDF) ont l'expérience de
l'utilisation d'outils commerciaux d'analyse statique de programmes
parallèles. Ils n'en sont pas satisfaits à cause de l'imprécision des
analyses. Le projet THÉSÉE devrait permettre de lever les verrous
technologiques permettant de réaliser un outil applicable à l'analyse
statique de programmes asynchrones. De tels outils ne sont pas disponibles
et les bases théoriques (sémantiques, abstractions) sont encore manquantes
pour passer à l'échelle.

4) Partenaires, compétences

Le partenariat comprend les équipes d'interprétation abstraite de l'École
normale supérieure et de l'École polytechnique. Les partenaires
industriels (Airbus et EDF) ont une longue expérience de l'usage de
l'analyse statique par interprétation abstraite, qu'ils souhaitent voir
considérablement développer.

La valeur ajoutée du partenariat tient au fait que la difficulté n'est pas
tant de définir l'analyse statique de modèles simples des programmes
parallèles mais de le faire avec l'objectif d'aboutir à une solution
viable, servant de base à la réalisation d'un analyseur ut