Towards the Formal Verification of the functional architecture of Autonomous Satellite Onboard Flight Software
Michel Lemaı̂tre, Gérard Verfaillie · 2008
The AGATA project, jointly conducted by CNES and ONERA, investigates the possibility of ad-vanced autonomy for spacecraft. The flight software (FS) is a key component of such an au-tonomous spacecraft. We are currently investigating the use of the high level synchronous langage Esterel to design the reactive part of the FS. The choice of such a semantically well-defined lan-guage has many advantages. One of those is to open the verification process to formal methods. This article reports the effective use of a formal method and tool to verify some typical properties on the preliminary version of the FS for an autonomous observing satellite.