Formal Verification of Helicopter Automatic Landing Control Algorithm in Theorem Prover Coq
Volume 14, Number 9, September 2018, pp. 19471957 DOI: 10.23940/ijpe.18.09.p2.19471957
Xi Chen^{a} and Gang Chen^{b}^{}
^{a}College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, 210000, China ^{b}Beijing Jinghang Research Institute of Computing and Communication, Beijing, 100074, China
(Submitted on May 15, 2018; Revised on July 17, 2018; Accepted on August 10, 2018)
Abstract:
The helicopter flight control system plays an important role in helicopter flight and is known as the “brain” of the helicopter. Only when the system is verified correctly can the helicopter fly safely and steadily. This paper describes and validates the major part of an algorithm of automatic landing control in the highorder theorem prover Coq. Z transform is currently one of the most important flight control system analysis tools. This paper formally describes the definition of Z transform, validates some properties (i.e., homogeneous, uniformity, linear, and complex shift properties) of Z transform to extend the system analysis capabilities of theorem proving, and lays the foundation for further formalization of the helicopter flight control system.
References: 18
 S. Singgih and Wibowo, “Aircraft Flight Dynamics, Control and Simulation,” draft, 2007
 Y. D. Yang, Y. Huang, and L. H. Li, “Design of Automatic Transition and Hovering Flight Control System for Helicopter,” Journal of Nanjing University of Aeronautics & Astronautics, No. 2, pp. 200204, 2004
 Y. Bertot and P. Castran, “Interactive Theorem Proving and Program Development: Coq’Art the Calculus of Inductive Constructions,” pp. 137, Springer Publishing Company, 2004
 R. Inria, “The Coq Proof Assistant Reference Manual,” in Proceedings of First Annual Workshop on ComputerAided Verification, Vol. 4, No. 4, pp. 206207, 2003
 Y. D. Yang, “Helicopter Flight Control,” 2nd Edition, National Defense Industry Press, 2007
 S. S. Hu, “Principles of Automatic Control,” Beijing: Science Press, 2013
 Y. D. Yang, Y. Huang, and X. H. Wang, “Study on Explicit ModelFollowing and FlybyLight Control System for Hel icopter,” Acta Aeronautica ET Astronautica Sinica, No. 2, pp. 162164, 2004
 F. Y. Zheng and Y. D. Yang, “Flight Control System Design of Explicit ModelFollowing for Helicopter based on Control Distribution Matrix Decouple,” Journal of Naval Aeronautical and Astronautical University, No. 1, pp. 119124, 2007
 W. G. Kelley and A. C. Peterson, “Difference Equations: An Introduction with Applications,” Academic press, 2001
 D. V. Widder, “Laplace Transform (PMS6),” Princeton University Press, 2015
 S. Boldo, C. Lelay, and G. Melquiond, “Coquelicot: A UserFriendly Library of Real Analysis for Coq,” Mathematics in Computer Science, Vol. 9, No. 1, pp. 4162, 2015
 H. Tsumura, “An Elementary Proof of Euler's Formula for z (2m),” American Mathematical Monthly, Vol. 111, No. 5, pp. 430431, 2004
 G. X. Tang, “Theory and Application of Z Transform,” Beijing: Yuhang Press, September 1988
 G. J. Myers, C. Sandler, and T. Badgett, “The Art of Software Testing,” John Wiley & Sons, 2011
 U. Norell, “Towards a Practical Programming Language based on Dependent Type Theory,” pp. 1126, Sweden: Department of Computer Science and Engineering Chalmers University of Technology and Goteborg University, 1994
 A. Bove, P. Dybjer, and U. Norell, “A Brief Overview of Agda–A Functional Language with Dependent Types,” in Proceedings of International Conference on Theorem Proving in Higher Order Logics, pp. 7378, August 2009
 J. Harrison, “HOL Light: A Tutorial Introduction,” in Proceedings of International Conference on Formal Methods in ComputerAided Design, pp. 265269, Springer, Berlin, Heidelberg, November 1996
 U. Siddique, M. Y. Mahmoud and S. Tahar, “On the Formalization of ZTransform in HOL,” Interactive Theorem Proving, ITP 2014 Lecture Notes in Computer Science, Vol. 8558, Springer, Cham, 2014
Please note : You will need Adobe Acrobat viewer to view the full articles.
Attachments:
02IJPE0902.pdf  [Formal Verification of Helicopter Automatic Landing Control Algorithm in Theorem Prover Coq]  886 Kb 
