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

Résumé : 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.
Type de document :
Chapitre d'ouvrage
Mogensen, T. and Schmidt, D.A. and Sudborough, I.H. The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, 2566, Springer, pp.85-108, 2002, Lecture Notes in Computer Science, 〈10.1007/3-540-36377-7_5〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00528442
Contributeur : Jérôme Feret <>
Soumis le : jeudi 21 octobre 2010 - 17:02:34
Dernière modification le : jeudi 10 mai 2018 - 02:06:44

Lien texte intégral

Identifiants

Collections

Citation

Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, et al.. Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. Mogensen, T. and Schmidt, D.A. and Sudborough, I.H. The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, 2566, Springer, pp.85-108, 2002, Lecture Notes in Computer Science, 〈10.1007/3-540-36377-7_5〉. 〈inria-00528442〉

Partager

Métriques

Consultations de la notice

147