Astrée is a parametric Abstract Interpretation based static analyser that aims at proving the absence of RTE (Run-Time Errors) in control programs written in C. Such properties are clearly safety properties since the behaviour of a C program is undefined after a RTE. When it analyses a program of the class for which it is specialised, Astrée is far more precise than general purpose static analysers. Nevertheless, for safety and industrial reasons, the small number of false alarms first produced by the tool must be reduced down to zero by a new fine tuned analysis. Through the description of experiments made on real programs, the paper shows how Abstract Interpretation based static analysis will contribute to the safety of avionics programs and how a user from industry can achieve the false alarm reduction process via a dedicated method. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Souyris, J., & Delmas, D. (2007). Experimental assessment of Astrée on safety-critical avionics software. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4680 LNCS, pp. 479–490). Springer Verlag. https://doi.org/10.1007/978-3-540-75101-4_45
Mendeley helps you to discover research relevant for your work.