Skip to Main content Skip to Navigation
Conference papers

Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites

Abstract : We propose a new approach for modelling the functional behaviour of an Earth observation satellite. We leverage this approach in order to develop a safety critical software, a "telecommand verifier", that is in charge of checking onboard whether a sequence of instructions is safe for execution. This new service is needed in order to add more autonomy to satellites. To do so, we propose a new Domain Specific Modelling Language and the toolchain required for integration into an embedded software. This framework is based on the composition of deterministic finite state machines with safety conditions , timeouts, and transitions that accept durations as a parameter. It is able to generate code in the synchronous programming language Lustre from a high-level specification of the satellite. This gives a formal way to derive an event-based algorithm simulating the execution of telecommand sequence and, thereupon, a provably correct onboard verifier.
Complete list of metadata
Contributor : Silvano Dal Zilio <>
Submitted on : Friday, January 31, 2020 - 9:43:11 AM
Last modification on : Thursday, June 10, 2021 - 3:47:50 AM
Long-term archiving on: : Friday, May 1, 2020 - 1:17:16 PM


Files produced by the author(s)


  • HAL Id : hal-02462058, version 1
  • ARXIV : 2001.11875


Vincent Mussot, Silvano Dal Zilio, Loic Correnson, Serge Rainjonneau, Yves Bardout, et al.. Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites. 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020), Jan 2020, Toulouse, France. ⟨hal-02462058⟩



Record views


Files downloads