Applicability of Model Checking for Verifying Spacecraft Operational Designs

Guaranteeing safety and correctness is one of the main objectives during the development of space systems. This is a challenging task, since many different engineering disciplines are involved in the development and the constituent parts of a spacecraft are highly interconnected and interdependent. Increasingly, formal methods such as model checking are applied to verify safety-critical parts of spacecraft designs and also implementation, since they may prove the absence of design errors. Generally, a major challenge for adopting model checking into the design process is its scalability. Usually, the whole state space of a system, which grows exponentially with, e.g., the number of parallel processes, must be explored.In this paper, we consider operational designs of spacecraft as they may occur during early development phases and systematically evaluate the scalability of model checking for verifying such models. For this, we created an arbitrarily scalable operational design describing the mode management of a satellite. Transformations of the models into the modeling languages of different model-checking tools enables a comparative scalability study of various model-checking algorithms. The evaluation shows promising results for symbolic model-checking approaches. A comparatively low analysis time and memory usage suggest that model checking for early operational designs can be incorporated into existing design processes.