[1] S. Singgih and Wibowo, “Aircraft Flight Dynamics, Control and Simulation,” draft, 2007
[2] Y. D. Yang, Y. Huang,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,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,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,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,U. Norell, “A Brief Overview of Agda-A Functional Language with Dependent Types,” inProceedings of International Conference on Theorem Proving in Higher Order Logics, pp. 73-78, August 2009
[17] J. Harrison, “HOL Light: A Tutorial Introduction,” inProceedings 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 |
