Formal verification of lunar rover control software using UPPAAL

Lijun Shan, Yuying Wang, Ning Fu, Xingshe Zhou, Lei Zhao, Lijng Wan, Lei Qiao, Jianxin Chen

科研成果: 书/报告/会议事项章节会议稿件同行评审

5 引用 (Scopus)

摘要

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.

源语言英语
主期刊名FM 2014
主期刊副标题Formal Methods - 19th International Symposium, Proceedings
出版商Springer Verlag
718-732
页数15
ISBN(印刷版)9783319064093
DOI
出版状态已出版 - 2014
活动19th International Symposium on Formal Methods, FM 2014 - Singapore, 新加坡
期限: 12 5月 201416 5月 2014

出版系列

姓名Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
8442 LNCS
ISSN(印刷版)0302-9743
ISSN(电子版)1611-3349

会议

会议19th International Symposium on Formal Methods, FM 2014
国家/地区新加坡
Singapore
时期12/05/1416/05/14

指纹

探究 'Formal verification of lunar rover control software using UPPAAL' 的科研主题。它们共同构成独一无二的指纹。

引用此