Formal Modeling and Verification of Operational Flight Program in a Small-Scale Unmanned Helicopter

Formal verification has played an important role in demonstrating correctness of safety-critical systems. Small-scale unmanned helicopters have been increasingly developed for various purposes such as scientific exploration and commercial or defense applications. The HELISCOPE project in Korea aims to develop a small-scale unmanned helicopter and its onboard embedded computing system for flight control and real-time transmission of multimedia data. This paper shares the authors' experience on the formal verification of the operational flight program (OFP) developed in the project. Because the OFP provides real-time controls on various sensors and actuators, demonstration of its correctness through formal verifications has been strongly recommended. This paper focuses on real-time process communications among sensing processes, a monitoring process, and a controller process. They all share a common data area. Two different formal models were developed for the OFP and verified with the SPIN and UPPAAL model checkers. While the SPIN model checker is widely used for modeling and verifying communication protocols, the real-time behavior of the OFP controller needs more advanced techniques that can handle real-time properties explicitly, i.e., timed automata and the UPPAAL verification system. The verification of the OFP found several safety-critical faults; they were all reported to development teams and fixed. DOI: 10.1061/(ASCE)AS.1943-5525.0000165. (C) 2012 American Society of Civil Engineers.