Interprétation abstraite : application aux logiciels de l'A380.
Exposé sur des questions d'actualité, Académie des Sciences, Paris, France, 6 Juin 2006.
Les logiciels complexes comportant quasiment tous des erreurs, les chercheurs ont développé des méthodes de preuve de la correction des programmes. Ceci consiste à fournir une sémantique décrivant formellement les exécutions d'un programme puis à démontrer un théorème exprimant que ces exécutions ont une certaine propriété (comme par exemple qu'un résultat attendu est fourni en un temps fini). Des résultats mathématiques fondamentaux montrent qu'il n'est pas possible de faire faire ces preuves automatiquement par des ordinateurs.
Devant cette difficulté fondamentale, l'interprétation abstraite procède par approximation correcte de la sémantique. Si l'approximation est suffisamment grossière, elle est calculable par un ordinateur. Si elle est suffisamment fine, elle permet d'obtenir une preuve formelle de correction. L'objectif est donc de rechercher des approximations suffisamment précises et peu coûteuses à calculer.
Nous donnerons quelques éléments d'interprétation abstraite en expliquant comment formaliser l'abstraction de propriétés de sémantiques pour obtenir des approximations calculables conduisant à des algorithmes effectifs d'analyse statique des comportements possibles des programmes.
Finalement nous montrerons un exemple d'application de la théorie à la preuve de l'absence d'erreurs à l'exécution sur des programmes de contrôle/commande synchrones en soulignant les difficultés (comme le calcul flottant). Cette approche a été appliquée avec succès à la vérification du logiciel de commande de vol électrique de l'A380.
Interprétation abstraite, Sémantique, Abstraction, Approximation, Analyse statique, Erreurs à l'exécution.
Since almost any complex software has bugs, researchers have developed program correctness proof methods. This consists in defining a semantics formally describing the executions of a program and then in proving a theorem stating that these executions have a given property (for example that an expected result is provided in a finite time). Fundamental mathematical results show that these proofs cannot be done automatically by computers.
Confronted with this fundamental difficulty, abstract interpretation proceeds by correct approximation of the semantics. If the approximation is coarse enough, it is computable. If it is precise enough, it yields a correctness proof. The goal is therefore to find cheap approximations which are precise enough.
We will introduce a few elements of abstract interpretation and explain how to formalize the abstraction of semantic properties so as to obtain computable approximations leading to effective algorithms for the static analysis of the possible behaviours of programs.
Finally, we will describe an example of application of the theory to the proof of absence of runtime errors on synchronous control/command and underly the difficulties (such as floating point computations). This approach was applied with success to the verification of the electric flight control of the A380.
Abstract interrpetation, Semantics, Abstraction, Approximation, Static analysis, Runtime errors.
\bibitem{Cousot-AcadSci-06-06-06}
P.~Cousot.
\newblock Interpr\'etation abstraite~: application aux logiciels de l'{A380}.
\newblock \emph{Expos\'e sur des questions d'actualit\'e},
Acad\'emie des Sciences, Paris, France, 6 juin 2006.
@conference{Cousot-AcadSci-06-06-06,
author = {P{.} Cousot},
title = {Interpr\'etation abstraite~: application aux logiciels de l'{A380}},
note = {\emph{Expos\'e sur des questions d'actualit\'e},
Acad\'emie des Sciences, Paris, France},
month = {6 juin},
year = 2006,
}