  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.
