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


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
StatePublished - 2009
EventDASIA 2009 Conference on DAta Systems In Aerospace - Istanbul, Turkey
Duration: May 26 2009May 29 2009

Publication series

NameEuropean Space Agency, (Special Publication) ESA SP
Volume669 SP
ISSN (Print)0379-6566


OtherDASIA 2009 Conference on DAta Systems In Aerospace

ASJC Scopus subject areas

  • Aerospace Engineering
  • Space and Planetary Science


Dive into the research topics of 'Space software validation using abstract interpretation'. Together they form a unique fingerprint.

Cite this