Model checking aircraft controller software: a case study. (21st November 2013)

• Record Type: Journal Article
• Authors: Chen, Zhe; Gu, Yi; Huang, Zhiqiu; Zheng, Jun; Liu, Chang; Liu, Ziyi; Tse, T. H.; Gotlieb, Arnaud; Chen, Zhenyu
• Is Part Of: Software, practice & experience. Volume 45:Number 7(2015)
• Page Start: 989
• Page End: 1017
• Publication Date: 2013-11-21
• Subjects: Computer software -- Periodicals; Computer programming -- Periodicals; Computer programs -- Periodicals; 005.3
• DOI: 10.1002/spe.2242
• Languages: English
• ISSNs: 0038-0644

Abstract

<abstract abstract-type="main" id="spe2242-abs-0001"> <title>Summary</title> <p id="spe2242-para-0001">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 &amp; Sons, Ltd.</p> </abstract>