Abstract:
This paper reports the results of an ESA funded project on the use of abstract
interpretation to validate critical real-time embedded space software. Abstract
interpretation is industrially used since several years, especially for the
validation of the Ariane 5 launcher. However, the limitations of the tools
used so far prevented a wider deployment. Astrium Space Transportation, CEA,
and ENS have analyzed the performances of two recent tools on a case study
extracted from the safety software of the ATV:
- ASTRÉE, developed by ENS and CNRS, to check for run-time errors,
- FLUCTUAT, developed by CEA, to analyse the accuracy of numerical
computations.
The conclusion of the study is that the performance of
this new generation of tools has dramatically increased
(no false alarms and fine analysis of numerical
precision).
\bibitem{dasia09}
{\sc Bouissou, O., Conquet, E., Cousot, P., Cousot, R., Feret, J., Ghorbal, K.,
Goubault, E., Lesens, D., Mauborgne, L., Min\'e, A., Putot, S., Rival, X.,
and Turin, M.}
\newblock Space software validation using abstract interpretation.
\newblock In {\em Proc. of the Int. Space System Engineering Conf., Data
Systems in Aerospace (DASIA 2009)\/} (Istambul, Turkey, May 2009),
vol.~SP-669, ESA, pp.~1--7.
@inproceedings{dasia09,
author = {Olivier Bouissou and Eric Conquet and Patrick Cousot and
Radhia Cousot and J{\'e}r{\^o}me Feret and Khalil Ghorbal and
Eric Goubault and David Lesens and Laurent Mauborgne and
Antoine Min\'e and Sylvie Putot and Xavier Rival and Michel Turin},
title = {Space Software Validation using Abstract Interpretation},
pages = {1--7},
volume = {SP-669},
year = {2009},
month = {May},
address = {Istambul, Turkey},
booktitle = {Proc. of the Int. Space System Engineering Conf.,
Data Systems in Aerospace (DASIA 2009)},
publisher = {ESA},
}