A Model-Based Approach to Verification of Spacecraft Software Using the SPIN Model Checker

Abstract

Contemporary approaches to verification of embedded real-time systems, such as those fielded for deep-space science missions, are limited in their effectiveness. These approaches are typically characterized by an ad-hoc approach to test coverage and a strong reliance on system testbeds to demonstrate compliance with narrow, ill-defined success criteria. As a result of this lack of rigor, completeness of test efforts is determined not by an explicit demonstration of compliance with requirements but by informal metrics driven by schedule limitations. Furthermore, a ‘successful’ test in such a program constitutes only an existence proof of proper system behavior: it demonstrates a successful execution, but provides no assurances about the myriad possible execution traces. To address this limitation, we approach system verification by applying the technique of logic model checking, which allows formal statement of desired system properties, and provides an automatic verification tool that checks whether all system behaviors satisfy the desired properties. Model checking, however, presents its own unique challenges: (a) the system of interest must be modeled in a formalism usable by the checker, (b) the environment of interest must be modeled in a similar way, (c) properties to be verified must be formalized and expressed in the logic accepted by the checker, and (d) appropriate abstractions must be introduced to combat exponential growth of the search space as model size increases. A further complication that accompanies (a) is that as the original design changes, the model must be modified appropriately so that it faithfully represents the system. These challenges are not new; however, in the context of spacecraft system verification, there seem to be few documented instances of application of model checking to system verification. We report on experience with applying model checking to the verification of a complex fault protection scheme used on a recent robotic deep-space mission. Our approach is based on a clear division of labor between the systems engineers familiar with system design and high level properties and verification experts familiar with the modeling and verification tools being used. We describe how our approach enabled systems engineers to focus on the development of declarative, requirements-derived models while leaving the task of generating the executable specification models to the verification experts.