Probabilistic Model Checking applied to Autonomous Spacecraft Reconfiguration

Formal verification techniques are necessary to demonstrate the completeness, the correctness, and the consistency in implementing spacecraft model-based autonomy requirements, where we have to explore the behavior of the system over a large input range. This paper introduces an approach based on probabilistic model checking to verify the specification of spacecraft autonomous reconfiguration functionality, modeled via Markov Decision Process. Some preliminary results show how this approach can be used to check whether the system fulfills suitably-defined properties under a given probability.