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

摘要

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.