TY - GEN
T1 - An Empirical Study of Open Source Flight Control Software Program Model Checking
AU - Cao, Zhiqin
AU - Yin, Jinyu
AU - Wang, Yichen
AU - Li, Yu
AU - Zhang, Jintao
N1 - Publisher Copyright:
© 2019 IEEE.
PY - 2019/7
Y1 - 2019/7
N2 - The process of model checking generally involves: models construction, properties specifications, and using tools or algorithms for model checking. Unfortunately, in practice research, there are problems in every step of the model checking, such as the well-known state explosion problem. In order to summarize the experience and lessons in the practice of model checking, this paper selects open source flight control software MWC as the research object, and analyzes the problems encountered in the process of model checking: (1) modeling object selection, (2) state explosion, (3) model abstraction, (4) properties identification and specification, and corresponding solutions are given. The empirical study verified the ability of the model checking technology, and carried out the model checking on the MWC open source flight control software, and successfully detected the important errors.
AB - The process of model checking generally involves: models construction, properties specifications, and using tools or algorithms for model checking. Unfortunately, in practice research, there are problems in every step of the model checking, such as the well-known state explosion problem. In order to summarize the experience and lessons in the practice of model checking, this paper selects open source flight control software MWC as the research object, and analyzes the problems encountered in the process of model checking: (1) modeling object selection, (2) state explosion, (3) model abstraction, (4) properties identification and specification, and corresponding solutions are given. The empirical study verified the ability of the model checking technology, and carried out the model checking on the MWC open source flight control software, and successfully detected the important errors.
KW - flight control software
KW - formal specification
KW - model checking
KW - state explosion
UR - https://www.scopus.com/pages/publications/85073870739
U2 - 10.1109/QRS-C.2019.00043
DO - 10.1109/QRS-C.2019.00043
M3 - 会议稿件
AN - SCOPUS:85073870739
T3 - Proceedings - Companion of the 19th IEEE International Conference on Software Quality, Reliability and Security, QRS-C 2019
SP - 164
EP - 169
BT - Proceedings - Companion of the 19th IEEE International Conference on Software Quality, Reliability and Security, QRS-C 2019
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 19th IEEE International Conference on Software Quality, Reliability and Security Companion, QRS-C 2019
Y2 - 22 July 2019 through 26 July 2019
ER -