Paper Info
Title
Formal Verification of Lunar Rover Control Software Using UPPAAL.
Abstract
This paper reports our formal verification of Chinese Lunar Rover control software, an embedded real-time multitasking software system running over a home-made real-time operating system (RTOS). The main purpose of the verification is to validate if the system satisfies a time-related functional property. We modeled the RTOS, application tasks and physical environment as timed automata and analyzed the system using statistical model checking (SMC) of UPPAAL. Verification result showed that our model was able to track down undesired behavior in the multitasking system. Moreover, as the modeling framework we designed is general and extensible, it can be a reference method for verifying other real-time multitasking systems.
Year
DOI
Venue
2014
10.1007/978-3-319-06410-9_48
Lecture Notes in Computer Science
Keywords
Field
DocType
Formal Verification,Multitasking System,Statistical Model Checking
Functional verification,Computer science,Real-time operating system,Real-time computing,Runtime verification,Software system,Verification,Human multitasking,Formal verification,Embedded system,Software verification
Conference
Volume
ISSN
Citations 
8442
0302-9743
0
PageRank 
References 
Authors
0.34
6
8
Name
Order
Citations
PageRank
LiJun Shan1958.85
Yuying Wang200.34
Ning Fu343.02
Xingshe Zhou41621136.85
Lei Zhao500.34
Lijng Wan600.34
Lei Qiao725.43
Jianxin Chen800.34