Formal Verification in Early Mission Planning

Spacecraft are complex systems. Changing one of its design parameter can have implications on the overall design and might become a crucial factor to mission success. In the early phases of spacecraft design, parameters as well as the mission goals are likely to change. These changes have to be applied carefully and need to be analyzed in respect to the whole system and the intended mission. The software Virtual Satellite supports this analysis by using an abstract model where the engineers can enter design data of their components. It allows describing operational phases of the spacecraft by defining modes such as Recharge or Science. These operational modes can be referenced by parameters to define individual values for them. Together with their respective mode durations, it can be determined for example how much energy is consumed in a specific mode or how much is produced. But this does not consider the influence of the parameter with respect to the overall mission goals. For example having a mission life time of 20 years and a spacecraft which spends too much of that time to maintain its power state, it remains unclear if the remaining time is long enough to gather enough scientific data as demanded by the mission requirements. This paper shows an approach to such problems based on formal verification. The data of the early phase model is used to create a state model of the spacecraft. Both, the model and the formalized requirements will be given to a model checker that automatically verifies on formal basis that the spacecraft complies with its specification. This method enables engineers to quickly check the design with respect to the mission requirements once they applied changes to it or to the requirements