Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software

We report on a successful preliminary experience in the design and implementation of a special-purpose Abstract Interpretation based static program analyzer for the verification of safety critical embedded real-time software. The analyzer is both precise (zero false alarm in the considered experiment) and efficient (less than one minute of analysis for 10,000 lines of code). Even if it is based on a simple interval analysis, many features have been added to obtain the desired precision: expansion of small arrays, widening with several thresholds, loop unrolling, trace partitioning, relations between loop counters and other variables. The efficiency of the tool mainly comes from a clever representation of abstract environments based on balanced binary search trees.Nous rapportons sur une expérience préliminaire fructueuse sur la conceptionet l'implantation d'un analyseur statique de programmes, basé sur l'interprétation abstraite, pour la vérification de l'absence d'erreurs à l'exécution dans des logiciels critiques embarqués temps-réel. L'analyseur est à la fois précis (aucune fausse alarme dans l'expérimentation considérée) et efficace (moins d'une minute de temps d'analyse pour 10 000 lignes de code). Même s'il est basé sur une simple analyse d'intervalles, de nombreuses extensions à cette analyse classique ont été introduites pour obtenir de telles performances : expansion des petits tableaux, élargissements étagés, dépliages de boucles, partitionnement de traces, relation entre compteurs de boucle et autres variables. L'efficacité de l'outil vient d'une représentation astucieuse des environnements abstraits basée sur des applications fonctionnelles implantées par des arbres binaires de recherche équilibrés