A symbolic model checking approach to verifying satellite onboard software |
| |
Affiliation: | Aalto University, School of Science, Department of Information and Computer Science, PO Box 15400, FI-00076 Aalto, Finland;Newcastle University |
| |
Abstract: | 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. |
| |
Keywords: | Symbolic model checking AOCS NuSMV 2 Liveness Safety |
本文献已被 ScienceDirect 等数据库收录! |
|