An Empirical Study of Open Source Flight Control Software Program Model Checking

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.