Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites
This work addresses the need for increased autonomy in satellites by providing a safety-critical verification method, though it is incremental as it builds on existing formal methods for embedded systems.
The paper tackles the problem of verifying the safety of autonomous command sequences for Earth observation satellites by proposing a formal modeling approach, resulting in a provably correct onboard telecommand verifier that can check instruction sequences before execution.
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.