@inproceedings{7985c6a3df1649509c22d81faff3ffc1,
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.",
keywords = "Formal Verification, Multitasking System, Statistical Model Checking",
author = "Lijun Shan and Yuying Wang and Ning Fu and Xingshe Zhou and Lei Zhao and Lijng Wan and Lei Qiao and Jianxin Chen",
year = "2014",
doi = "10.1007/978-3-319-06410-9_48",
language = "英语",
isbn = "9783319064093",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "718--732",
booktitle = "FM 2014",
note = "19th International Symposium on Formal Methods, FM 2014 ; Conference date: 12-05-2014 Through 16-05-2014",
}