A symbolic model checking approach to verifying satellite onboard software

• The Ada code implementation of a mission-critical satellite software system is modeled.
• The specification is translated into several linear temporal logic (LTL) formulas.
• The model is checked against the LTL properties using the NuSMV 2 model checker.
• A new acceptance-counting approach for LTL property model checking is presented.
• Our new method efficiently proves all the specified properties of the system.

This paper discusses the use of symbolic model checking technology to verify the design of an embedded satellite software control system called the attitude and orbit control system (AOCS). This system is mission critical because it is responsible for maintaining the attitude of the satellite and for performing fault detection, isolation, and recovery decisions. An executable AOCS implementation by Space Systems Finland has been provided in Ada source code form, and we use the input language of the symbolic model checker NuSMV 2 to model the implementation at a detailed level. We describe the modeling techniques and abstractions used to alleviate the state space explosion due to the handling of timers and the large number of system components controlled by the AOCS. The required behavior has been specified as extended state machine diagrams and translated to temporal logic properties. Besides well-known LTL and CTL model checking algorithms, we adapt a previously unexplored form of the liveness-to-safety approach to the problem. The latter new technique turns out to successfully prove all desired properties of the system, outperforming both the LTL and CTL implementations of NuSMV 2.