Vérification de logiciels critiques
Étant donné les conséquences catastrophiques d'une erreur dans un
logiciel critique, embarqué dans une voiture ou un avion par exemple,
la vérification et la validation est particulièrement importante pour
de tels logiciels. L'analyse statique est utile pour atteindre cet
objectif, puisqu'elle peut donner des preuves que le logiciel
satisfait les propriétés désirées.
Toute l'équipe interprétation abstract de l'École Normale Supérieure,
avec Radhia Cousot de l'École Polytechnique, ont conçu et implémenté
un analyseur qui verifie l'absence d'erreurs à l'exécution (division
par zéro, dépassements de capacité, etc) dans des programmes C.
Cet analyseur est efficace (1h40min pour analyser un programme industriel
d'environ 75000 lignes) et atteint un niveau de précision sans précédent
(seulement 11 fausses alarmes sur ce programme). Ce travail est fait dans
le cadre du projet
Astrée, en collaboration avec Airbus France.
Page officielle sur le projet Astrée
Publications sur ce sujet
-
[1]
-
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent
Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival.
A Static Analyzer for Large Safety-Critical
Software.
In ACM SIGPLAN 2003 Conference on Programming Language Design
and Implementation (PLDI'03),
pages 196-207, San Diego, California, June 2003. ACM.
-
[2]
-
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent
Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival.
Design and Implementation of a Special-Purpose
Static Program Analyzer for Safety-Critical Real-Time
Embedded Software, invited chapter.
In T. Mogensen, D. A. Schmidt, and I. H. Sudborough, editors,
The Essence of Computation: Complexity, Analysis, Transformation. Essays
Dedicated to Neil D. Jones, volume 2566 of Lecture Notes in Computer
Science, pages 85-108. Springer, December 2002.
Bruno Blanchet