Paper Info
Title
A symbolic model checking approach to verifying satellite onboard software
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.
Year
DOI
Venue
2011
10.1016/j.scico.2013.03.005
Science of Computer Programming
Keywords
DocType
Volume
verifying satellite onboard software,ctl implementation,ctl model checking algorithm,ada source code form,symbolic model checking technology,symbolic model checking approach,extended state machine diagram,embedded satellite software control,symbolic model checker,system component,executable aocs implementation,orbit control system
Journal
82,
ISSN
Citations 
PageRank 
0167-6423
9
0.55
References 
Authors
16
3
Name
Order
Citations
PageRank
Xiang Gan190.55
Jori Dubrovin2644.53
Keijo Heljanko375147.90