Space software validation using abstract interpretation

Olivier Bouissou, Eric Conquet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Khalil Ghorbal, Eric Goubault, David Lesens, Laurent Mauborgne, Antoine Miné, Sylvie Putot, Xavier Rival, Michel Turin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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).

Original languageEnglish (US)
Title of host publicationProceedings of DASIA 2009 Conference on DAta Systems In Aerospace
Volume669 SP
StatePublished - 2009
EventDASIA 2009 Conference on DAta Systems In Aerospace - Istanbul, Turkey
Duration: May 26 2009May 29 2009

Other

OtherDASIA 2009 Conference on DAta Systems In Aerospace
CountryTurkey
CityIstanbul
Period5/26/095/29/09

Fingerprint

computer programs
software
space transportation
launchers
false alarms
safety
European Space Agency
analysis
alarm
project

ASJC Scopus subject areas

  • Aerospace Engineering
  • Space and Planetary Science

Cite this

Bouissou, O., Conquet, E., Cousot, P., Cousot, R., Feret, J., Ghorbal, K., ... Turin, M. (2009). Space software validation using abstract interpretation. In Proceedings of DASIA 2009 Conference on DAta Systems In Aerospace (Vol. 669 SP)

Space software validation using abstract interpretation. / Bouissou, Olivier; Conquet, Eric; Cousot, Patrick; Cousot, Radhia; Feret, Jérôme; Ghorbal, Khalil; Goubault, Eric; Lesens, David; Mauborgne, Laurent; Miné, Antoine; Putot, Sylvie; Rival, Xavier; Turin, Michel.

Proceedings of DASIA 2009 Conference on DAta Systems In Aerospace. Vol. 669 SP 2009.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Bouissou, O, Conquet, E, Cousot, P, Cousot, R, Feret, J, Ghorbal, K, Goubault, E, Lesens, D, Mauborgne, L, Miné, A, Putot, S, Rival, X & Turin, M 2009, Space software validation using abstract interpretation. in Proceedings of DASIA 2009 Conference on DAta Systems In Aerospace. vol. 669 SP, DASIA 2009 Conference on DAta Systems In Aerospace, Istanbul, Turkey, 5/26/09.
Bouissou O, Conquet E, Cousot P, Cousot R, Feret J, Ghorbal K et al. Space software validation using abstract interpretation. In Proceedings of DASIA 2009 Conference on DAta Systems In Aerospace. Vol. 669 SP. 2009
Bouissou, Olivier ; Conquet, Eric ; Cousot, Patrick ; Cousot, Radhia ; Feret, Jérôme ; Ghorbal, Khalil ; Goubault, Eric ; Lesens, David ; Mauborgne, Laurent ; Miné, Antoine ; Putot, Sylvie ; Rival, Xavier ; Turin, Michel. / Space software validation using abstract interpretation. Proceedings of DASIA 2009 Conference on DAta Systems In Aerospace. Vol. 669 SP 2009.
@inproceedings{5d01015e354c46a9bdb0dbcd09e5614a,
title = "Space software validation using abstract interpretation",
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}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).",
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",
year = "2009",
language = "English (US)",
isbn = "9789292212339",
volume = "669 SP",
booktitle = "Proceedings of DASIA 2009 Conference on DAta Systems In Aerospace",

}

TY - GEN

T1 - Space software validation using abstract interpretation

AU - Bouissou, Olivier

AU - Conquet, Eric

AU - Cousot, Patrick

AU - Cousot, Radhia

AU - Feret, Jérôme

AU - Ghorbal, Khalil

AU - Goubault, Eric

AU - Lesens, David

AU - Mauborgne, Laurent

AU - Miné, Antoine

AU - Putot, Sylvie

AU - Rival, Xavier

AU - Turin, Michel

PY - 2009

Y1 - 2009

N2 - 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).

AB - 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).

UR - http://www.scopus.com/inward/record.url?scp=74549162684&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=74549162684&partnerID=8YFLogxK

M3 - Conference contribution

SN - 9789292212339

VL - 669 SP

BT - Proceedings of DASIA 2009 Conference on DAta Systems In Aerospace

ER -