Username   Password       Forgot your password?  Forgot your username? 


Formal Verification of Helicopter Automatic Landing Control Algorithm in Theorem Prover Coq

Volume 14, Number 9, September 2018, pp. 1947-1957
DOI: 10.23940/ijpe.18.09.p2.19471957

Xi Chena and Gang Chenb

aCollege of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, 210000, China
bBeijing 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)


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 high-order 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

            1. S. Singgih and Wibowo, “Aircraft Flight Dynamics, Control and Simulation,” draft, 2007
            2. 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. 200-204, 2004
            3. Y. Bertot and P. Castran, “Interactive Theorem Proving and Program Development: Coq’Art the Calculus of Inductive Constructions,” pp. 1-37, Springer Publishing Company, 2004
            4. R. Inria, “The Coq Proof Assistant Reference Manual,” in Proceedings of First Annual Workshop on Computer-Aided Verification, Vol. 4, No. 4, pp. 206-207, 2003
            5. Y. D. Yang, “Helicopter Flight Control,” 2nd Edition, National Defense Industry Press, 2007
            6. S. S. Hu, “Principles of Automatic Control,” Beijing: Science Press, 2013
            7. Y. D. Yang, Y. Huang, and X. H. Wang, “Study on Explicit Model-Following and Fly-by-Light Control System for Hel icopter,” Acta Aeronautica ET Astronautica Sinica, No. 2, pp. 162-164, 2004
            8. F. Y. Zheng and Y. D. Yang, “Flight Control System Design of Explicit Model-Following for Helicopter based on Control Distribution Matrix Decouple,” Journal of Naval Aeronautical and Astronautical University, No. 1, pp. 119-124, 2007
            9. W. G. Kelley and A. C. Peterson, “Difference Equations: An Introduction with Applications,” Academic press, 2001
            10. D. V. Widder, “Laplace Transform (PMS-6),” Princeton University Press, 2015
            11. S. Boldo, C. Lelay, and G. Melquiond, “Coquelicot: A User-Friendly Library of Real Analysis for Coq,” Mathematics in Computer Science, Vol. 9, No. 1, pp. 41-62, 2015
            12. H. Tsumura, “An Elementary Proof of Euler's Formula for z (2m),” American Mathematical Monthly, Vol. 111, No. 5, pp. 430-431, 2004
            13. G. X. Tang, “Theory and Application of Z Transform,” Beijing: Yuhang Press, September 1988
            14. G. J. Myers, C. Sandler, and T. Badgett, “The Art of Software Testing,” John Wiley & Sons, 2011
            15. U. Norell, “Towards a Practical Programming Language based on Dependent Type Theory,” pp. 11-26, Sweden: Department of Computer Science and Engineering Chalmers University of Technology and Goteborg University, 1994
            16. 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. 73-78, August 2009
            17. J. Harrison, “HOL Light: A Tutorial Introduction,” in Proceedings of International Conference on Formal Methods in Computer-Aided Design, pp. 265-269, Springer, Berlin, Heidelberg, November 1996
            18. U. Siddique, M. Y. Mahmoud and S. Tahar, “On the Formalization of Z-Transform 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.Get Free Adobe Reader

                      This site uses encryption for transmitting your passwords.