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

doi:10.1007/978-3-319-06410-9_48

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

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

5 Scopus citations

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.

Original language	English
Title of host publication	FM 2014
Subtitle of host publication	Formal Methods - 19th International Symposium, Proceedings
Publisher	Springer Verlag
Pages	718-732
Number of pages	15
ISBN (Print)	9783319064093
DOIs	https://doi.org/10.1007/978-3-319-06410-9_48
State	Published - 2014
Event	19th International Symposium on Formal Methods, FM 2014 - Singapore, Singapore Duration: 12 May 2014 → 16 May 2014

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8442 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	19th International Symposium on Formal Methods, FM 2014
Country/Territory	Singapore
City	Singapore
Period	12/05/14 → 16/05/14

Keywords

Formal Verification
Multitasking System
Statistical Model Checking

Access to Document

10.1007/978-3-319-06410-9_48

Cite this

Shan, L., Wang, Y., Fu, N., Zhou, X., Zhao, L., Wan, L., Qiao, L., & Chen, J. (2014). Formal verification of lunar rover control software using UPPAAL. In FM 2014: Formal Methods - 19th International Symposium, Proceedings (pp. 718-732). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8442 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-06410-9_48

@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",

}

Shan, L, Wang, Y, Fu, N, Zhou, X, Zhao, L, Wan, L, Qiao, L & Chen, J 2014, Formal verification of lunar rover control software using UPPAAL. in FM 2014: Formal Methods - 19th International Symposium, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8442 LNCS, Springer Verlag, pp. 718-732, 19th International Symposium on Formal Methods, FM 2014, Singapore, Singapore, 12/05/14. https://doi.org/10.1007/978-3-319-06410-9_48

Formal verification of lunar rover control software using UPPAAL. / Shan, Lijun; Wang, Yuying; Fu, Ning et al.
FM 2014: Formal Methods - 19th International Symposium, Proceedings. Springer Verlag, 2014. p. 718-732 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8442 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Formal verification of lunar rover control software using UPPAAL

AU - Shan, Lijun

AU - Wang, Yuying

AU - Fu, Ning

AU - Zhou, Xingshe

AU - Zhao, Lei

AU - Wan, Lijng

AU - Qiao, Lei

AU - Chen, Jianxin

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

KW - Formal Verification

KW - Multitasking System

KW - Statistical Model Checking

UR - http://www.scopus.com/inward/record.url?scp=84958527587&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-06410-9_48

DO - 10.1007/978-3-319-06410-9_48

M3 - 会议稿件

AN - SCOPUS:84958527587

SN - 9783319064093

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 718

EP - 732

BT - FM 2014

PB - Springer Verlag

T2 - 19th International Symposium on Formal Methods, FM 2014

Y2 - 12 May 2014 through 16 May 2014

ER -

Shan L, Wang Y, Fu N, Zhou X, Zhao L, Wan L et al. Formal verification of lunar rover control software using UPPAAL. In FM 2014: Formal Methods - 19th International Symposium, Proceedings. Springer Verlag. 2014. p. 718-732. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-06410-9_48

Formal verification of lunar rover control software using UPPAAL

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this