Preliminary Study Of Coq-Based Formal Helicopter Filght Control Mathematics

The theorem proving is a branch of artificial intelligence.Its research goal is to prove the mathematical theorem with computer aid.Formal verification techniques based on theorem proving have been widely used in the proof and verification of mathematical theorems and software correctness verification.However,the application of theorem proof technique in engineering mathematics is still very rare.The safety flight control system plays an important role in flight control and is considered the "brain" of the aircraft.Only the system is verified to be correct can the aircraft fly safely and steadily.The flight control algorithm is the core of the flight control system.It is based on a large number of complicated calculus mathematical derivations.The correctness of these mathematical derivations plays a key role in the safety of the flight control system.The failure of the Mars lander was caused by mistakes in the decline process control in Europe.In the formal verification of helicopter flight control mathematics,there is currently a gap in the international arena.In this paper,based on the theorem prover Coq,the formal verification of the derivation of some mathematical formulas in the helicopter flight control system is carried out.The main research contents are as follows:First,the automatic transition flight control process of the helicopter based on the explicit model following control system is verified.This process is divided into two aspects: high transition and speed transition.The height is divided into two stages: parabolic falling and index flattening.These two phases are themselves constrained by the corresponding laws of physics and control objectives,requiring a smooth connection between the two.The mathematical formulas satisfied by the descent curve are derived from the derivation under these constraints.We have formalized and validated this derivation process.Second,verify the takeoff process and trajectory generation on the helicopter.The process is divided into three time periods,namely,the start phase,the steady rise phase and the final segment in time.It is simplified in space to ignore the Y-axis and only considers the XOZ plane.In the plane,the initial state and the task are required to ensure the smoothness of the trajectory and set the equation of motion below.During the verification process we proved several custom small lemmas.Third,verify the helicopter landing process and trajectory generation.Landing is more difficult than taking off on a ship because three factors are considered: the deck size is limited,the ship is shaking,and the helicopter’s own control is weakened.Fourth,Z-transformation formal verification.Z-transformation can transform a series of real or complex discrete signals from time domain to complex domain,which is an important analytical tool in control systems.Since the theorem of complex numbers in the Coq standard library and the thirdparty library is relatively lacking,we start from the formalization of complex numbers,convert and simplify the complex numbers by means of Euler’s formula,and then verify the homogeneity of the Ztransform on this basis.Uniform,linear,and complex displacement properties,thereby extending the ability of the theorem proving tool in system analysis,and laying the foundation for further formal helicopter flight control systems.