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.
\bibitem{erts10}
{\sc K{\"a}stner, D., Wilhelm, S., Nenova, S., Cousot, P., Cousot, R., Feret, J., Min{\'e}, A., Mauborgne, L., and Rival, X.}
\newblock Astr{\'e}e: Proving the Absence of Runtime Errors.
\newblock In {\em Embedded Real Time Software and Systems - ERTSS 2010.\/}
(2010).
@inproceedings{erts10,
author = "Daniel K{\"a}stner and Stephan Wilhelm and Stefana Nenova and
Patrick Cousot and Radhia Cousot and J{\'e}r{\^o}me Feret and
Antoine Min{\'e} and Laurent Mauborgne and Xavier Rival",
title = "Astr{\'e}e: Proving the Absence of Runtime Errors",
booktitle = "Embedded Real Time Software and Systems - ERTSS 2010",
year = 2010,
}