Formal Derivation and Verification of Coordinate Transformations in Theorem Prover Coq
Zhenwei Ma, Gang Chen · 2017
Transformation matrices of coordinate systems form a basic building block in flight control systems, their reliability has a significant impact on flight safety. There are five kinds of well-known coordinate systems used in flight control system design and there are 20 kinds of transformation matrices between them, many of which are fairly complex and have not been reported in popular flight control literature. This paper describes a method of formal derivation and verification of coordinate transformation matrices of aircraft control system using theorem prover Coq. We explain how to define and validate the transformation matrices in Coq, and describe techniques for the simplification of the verification process. This is one of our initial steps towards the formal study of flight control mathematics, laying the foundation of formal development of reliable flight control software.