P. Cousot, Vérification de logiciel embarqués critiques par interprétation abstraite.

Patrick Cousot.
Vérification de logiciel embarqués critiques par interprétation abstraite. $fran\347ais$
Séminaire du LINA, Laboratoire d'informatique de Nantes Atlantique, Nantes, France, 20 décembre 2007.

Résumé :
Les difficultés avec les méthodes formelles sont qu'elles requièrent une spécification formelle, une sémantique formelle du langage de programmation et, à cause de l'indécidabilité, présentent de sérieuses limitations sur la vérification automatique que la sémantique du programme satisfait la spécification. Les démonstrateurs de théorèmes ont besoin d'une assistance humaine tandis que la vérification exhaustive de modèles nécessite des modèles finis qui, sauf peut-être pour des composants matériels, sont généralement incomplets.
L'analyse statique offre une alternative intéressante, complètement automatique, en particulier quand la spécification peut être choisie implicitement. C'est le cas par exemple de la preuve d'absence d'erreurs à l'excution pour laquelle l'utilisateur n'a pas besoin de donner une spécification complexe. De plus l'analyse statique prend en compte des modèles infinis des calculs du programme directement calculés à partir du texte du programme de sorte que l'utilisateur n'a aucun besoin de fournir un modèle fini du programme et de son environnement d'exécution. Finalement les états accessibles en cours d'exécution sont calculés approximativement par une sur-approximation qui n'omet aucun cas possible. Par conséquent les questions délicates de sémantiques des programmes peuvent être résolues en considérant une approximation de tous les cas possibles. De par cette sur-approximation, aucune erreur ne peut être oubliée.
Si cette idée d'approximation permet de traiter les problèmes d'indécidabilité, elle a l'inconvénient majeur de prendre en compte des exécutions du programme qui sont fictives, sans aucune exécution correspondante observable dans les conditions d'exploitation du programme. Ces exécutions fictives, dont l'analyse ne peut déterminer si elles sont fictives ou observables, peuvent être à l'origine d'erreurs à l'exécution, qui doivent donc être signalées et constituent des « fausses alarmes » puisqu'elle correspondent à des exécutions fictives du programme . En général ces fausses alarmes doivent être résolues par inspection manuelle du code ce qui est extrêmement coûteux. Tout le problème est donc de choisir des abstractions de la sémantique du programme qui ne produisent pas ou peu de fausses alarmes. Pour ce faire, on peut restreindre la famille des programmes à analyser à un domaine d'application particulier de façon à adapter exactement les abstractions aux structures de données, primitives de calcul et schémas d'algorithmes spécifiques à ce domaine d'application.
Nous présenterons les éléments de la théorie de l'interprétation abstraite sur lesquelles reposent la correction de la notion d'approximation en analyse statique. Puis nous introduirons l'analyseur statique ASTRÉE (www.astree.ens.fr), qui est spécialisé dans la vérification de l'absence d'erreurs à l'exécution pour les programmes de contrôle/commande. L'analyseur utilise des abstractions générales (comme les intervalles, les octogones, le partitionnement de données et du contrôle) ainsi que des abstractions spécifiques au domaine d'applications (par exemple pour traiter les filtres ou l'accumulation potentielle d'erreurs d'arrondi). Finalement nous rendrons compte de l'application réussie d'ASTRÉE à la preuve d'absence d'erreurs à l'exécution dans des logiciels récents de commande de vol électrique.

Les transparents de l'exposé de 60 mn sont disponibles en format PDF, 4 transparents par page A4 orientée en paysage, à visionner avec Acrobat Reader
- pdf (2 Mb)

Référence bibliographique:

\bibitem{Cousot-Nantes07}
P.~Cousot.
\newblock V\'erification de logiciels embarqu\'es critiques par 
          interpr\'etation abstraite.
\newblock \emph{S\'eminaire du LINA, Laboratoire d'informatique de Nantes 
          Atlantique}, Nantes, France, 20 d\'ecembre 2007.

@inProceedings{Cousot-Nantes07,
   author =    {P{.} Cousot},
   title =     {V\'erification de logiciels embarqu\'es critiques par 
                interpr\'etation abstraite},
   booktitle = {S\'eminaire du LINA, Laboratoire d'informatique de Nantes 
                Atlantique},
   address =   {Nantes, France},
   month =     {20 d\'ecembre},
   year =      2007,
}

copyright notice
Last modified: Monday, 04-Jan-2010 13:56:00 CET