CaSSIS-CheckTC

About

Telecommands are instructions sent from ground control centers to manage scientific instruments during a mission. Verifying telecommand sequences before uplinking them to the spacecraft involves checking intended sequences against requirements that such sequences need to satisfy. Such telecommand requirements, elicited from mission operators, reflect operational constraints, mission requirements and safety protocols in place. This is a largely manual process that involves domain knowledge and expertise by mission officers.

The goal of CaSSIS-CheckTC consists of providing appropriate tool support to assist mission operators in verifying TC sequences in an automated way, allowing them to catch errors before sending telecommands to the spacecraft. We seek to first (i) elicit and then (ii) express desired TC requirements as temporal logic formulae in order to (iii) enable their automated verification via trace checking. When operators prepare a new telecommand sequence (reflecting, e.g., some new experiment), they can use appropriate CaSSIS-CheckTC tooling to check it for validity against stated requirements. Any deviations, such as missing or out-of-order commands, can then be flagged as anomalies, indicating potential errors that could lead to undesired instrument states.

This project will leverage expertise of the  Planetary Imaging Group in the  Space Research and Planetology Division of the  Physikalisches Institut and the Software Engineering Group at the Institute of Computer Science, towards the verification of CaSSIS flight software. This is a goal that is highly interdisciplinary in nature, since expertise of both groups is involved.

This work is a continuation of CaSSIS-Verif.