Astree: Proving the Absence of Runtime Errors

Daniel Kästner 1 Stephan Wilhelm 1 Stefana Nenova 1 Patrick Cousot 2 Radhia Cousot 2 Jérôme Feret 3 Laurent Mauborgne 2 Antoine Miné 2 Xavier Rival 3
3 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : Safety-critical embedded software has to satisfy stringent quality requirements. Testing and validation consumes a large and growing fraction of development cost. The last years have seen the emergence of semantics-based static analysis tools in various application areas, from runtime error analysis to worst-case execution time prediction. Their appeal is that they have the potential to reduce testing effort while providing 100% coverage, thus enhancing safety. Static runtime error analysis is applicable to large industry-scale projects and produces a list of definite runtime errors and of potential runtime errors which might be true errors or false alarms. In the past, often only the definite errors were fixed because manually inspecting each alarm was too time-consuming due to a large number of false alarms. Therefore no proof of absence of runtime errors could be given. In this article the parameterizable static analyzer Astrée is presented. By specialization and parametrization Astrée can be adapted to the software under analysis. This enables Astrée to efficiently compute precise results. Astrée has sucessfully been used to analyze large-scale safety-critical avionics software with zero false alarms.
Type de document :
Communication dans un congrès
Laprie, J.C. Embedded real time software and systems - ERTS2 2010, May 2010, Toulouse, France. 2010, 〈http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0024_final.pdf〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00528600
Contributeur : Jérôme Feret <>
Soumis le : vendredi 22 octobre 2010 - 10:30:20
Dernière modification le : vendredi 25 mai 2018 - 12:02:05

Identifiants

  • HAL Id : inria-00528600, version 1

Collections

Citation

Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, et al.. Astree: Proving the Absence of Runtime Errors. Laprie, J.C. Embedded real time software and systems - ERTS2 2010, May 2010, Toulouse, France. 2010, 〈http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0024_final.pdf〉. 〈inria-00528600〉

Partager

Métriques

Consultations de la notice

349