- Résumé
 :
La vérification d'un logiciel consiste à démontrer
que toutes les exécutions d''un programme satisfont une
spécification. Dans le cas de l'analyseur statique ASTRÉE (http://www.astree.ens.fr/),
la spécification est implicite : aucune exécution ne peut
conduire à une “erreur à l'exécution”
(débordement de tableau, pointeur indéfini, division par
zéro, débordement arithmétique, etc.).
L'interprétation abstraite est une théorie de
l'abstraction, c'est-à-dire des approximations sûres permettant
de faire la preuve automatiquement en considérant des
sur-ensembles des comportements possibles du programme. Contrairement
aux méthodes de recherche d'erreurs comme le model-checking
borné ou le test, aucun cas possible n'est omis et la preuve
d'erreurs à l'exécution est donc mathématiquement
valide. Certaines exécutions dans la sur-approximation peuvent
conduire à une erreur sans pour autant correspondre à une
exécution réelle (encore dite concrète). On parle dans
ce cas d'une “fausse alarme”. Toute la difficulté du problème
indécidable de la vérification est de choisir des
approximations sûres sans aucune fausse alarme (les erreurs conduisent
à de vraies alarmes ne peuvent être éliminées
qu'en les corrigeant). Dans le cas d'ASTRÉE, les programmes
écrits en C sont des logiciels synchrones de contrôle
commande temps réel. ASTRÉE contient des
abstractions généralistes (intervalles, octogones, etc)
et des abstractions spécifiques au domaine d'application (avec
filtres, intégrateurs, divergences lentes à cause
d'erreurs d'arrondis, etc). Cette adaptation au domaine d'application
a permis de vérifier formellement l'absence d'erreurs à
l'exécution dans des logiciels avioniques critiques de grande
taille, une première mondiale.
- Abstract:
Software verification consists in proving that executions of the
software in any admissible execution environment all satisfy a formal
specification. In the case of the ASTRÉE static analyser (http://www.astree.ens.fr/),
the specification is implicit: no execution can lead to a
“runtime error” (RTE) (such as buffer overrun, dangling
pointer, division by zero, float overflow, modular integer arithmetic
overflow, etc). The ASTRÉE
static analyser is designed by abstract interpretation of the semantics
of a subset of the C programming language (without dynamic memory
allocation, recursive function calls, no system and library calls as
found in most embedded software). Abstract interpretation is a theory
of abstraction, that is to say of safe approximation allowing for
automatic formal proofs by considering an over-approximation of the set
of all possible executions of the program. Contrary to bug-finding
methods (e.g. by test, bounded model-checking or error pattern search),
no potential error is ever omitted. Hence the proof of satisfaction of
the specification is mathematically valid. However, some executions
considered in the abstract, that is in the over-approximation, might
lead to an error while not corresponding to a concrete, that is actual,
execution. This spurious execution is then said to lead to a ``false
alarmÕÕ. All the difficulty of the undecidable verification problem is
therefore to design safe/sound over-approximations that are coarse
enough to be effectively computable by the static analyzer and precise
enough to avoid false alarms (the errors leading to true alarms can
only be eliminated by correcting the program that does not satisfy the
specification). In practice, knowing only the over-approximation
computed by the static analyser, it is difficult to distinguish false
alarms from actual ones. So the radical solution is to reach
zero false alarm which provides a full verification. To do so, ASTRÉE is specialized both
to precise program properties (i.e. RTEs) and a precise family of C
programs (i.e. real-time synchronous control/command C applications
preferably automatically generated from a synchronous language). The ASTRÉE static analyser uses
generalist abstractions (like intervals, octagons, decision trees,
symbolic execution, etc) and abstractions for the specific application
domain (to cope with filters, integrators, slow divergences due to
rounding errors, etc). Since 2003, these domain-specific abstractions allowed for
the verification of the absence of RTEs in several large avionic software, a
world première.
|
 |