Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proc. ACM SIGPLAN 2003 Conf. PLDI, San Diego, CA, US, 7–14 June 2003, pp. 196–207. ACM Press, New York (2003)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRE’E analyser. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Cousot, P.: Interprétation abstraite. Technique et Science Informatique 19(1-2-3), 155–164 (2000)
Cousot, P.: Abstract Interpretation Based Formal Methods and Future Challenges. In: Wilhelm, R. (ed.) Informatics. LNCS, vol. 2000, pp. 138–156. Springer, Heidelberg (2001)
Cousot, P., Cousot, R.: Basic Concepts of Abstract Interpretation. In: Jacquard, R. (ed.) Building the Information Society, pp. 359–366. Kluwer Academic Publishers, Dordrecht (2004)
Souyris, J., Le Pavec, E., Himbert, G., Jégu, V., Borios, G., Heckmann, R.: Computing the worst case execution time of an avionics program by abstract interpretation. In: Proceedings of the 5th Intl Workshop on Worst-Case Execution Time (WCET) Analysis, pp. 21–24 (2005)
Goubault, E., Martel, M., Putot, S.: Static Analysis-Based Validation of Floating-Point Computations. In: Alt, R., Frommer, A., Kearfott, R.B., Luther, W. (eds.) Numerical Software with Result Verification. LNCS, vol. 2991, pp. 306–313. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Souyris, J., Delmas, D. (2007). Experimental Assessment of Astrée on Safety-Critical Avionics Software. In: Saglietti, F., Oster, N. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2007. Lecture Notes in Computer Science, vol 4680. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75101-4_45
Download citation
DOI: https://doi.org/10.1007/978-3-540-75101-4_45
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75100-7
Online ISBN: 978-3-540-75101-4
eBook Packages: Computer ScienceComputer Science (R0)