Premium
Model checking aircraft controller software: a case study
Author(s) -
Chen Zhe,
Gu Yi,
Huang Zhiqiu,
Zheng Jun,
Liu Chang,
Liu Ziyi
Publication year - 2015
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/spe.2242
Subject(s) - correctness , computer science , model checking , interrupt , software , programming language , software engineering , component (thermodynamics) , unit testing , software verification , software construction , software system , embedded system , physics , thermodynamics , microcontroller
Summary This paper documents an application of model checking to formally verify an interrupt‐driven Slats and Flaps Control Unit software programmed in C, one component of a certain type of Chinese aircraft. Our objective was to identify errors rather than to prove correctness. We focused on the correctness of the algorithms used in the buffer operations, which are very common and important in aircraft software. In the verification, a total of four flawed code fragments was identified, including a minor efficiency issue. According to the programming team, this is regarded as a very successful result, and this project is the first successful attempt to apply model checking to the practice of verifying onboard aircraft software in China. Thanks to its completeness and reality, this case study can also serve as a complete and valuable real‐world example for teaching and learning model checking. Copyright © 2013 John Wiley & Sons, Ltd.