Verification framework for control theory of aircraft

A control system verification framework is presented for unmanned aerial vehicles using theorem proving. The framework's aim is to set out a procedure for proving that the mathematically designed control system of the aircraft satisfies robustness requirements to ensure safe performance under varying environmental conditions. Extensive mathematical derivations, which have formerly been carried out manually, are checked for their correctness on a computer. To illustrate the procedures, a higher-order logic interactive theorem-prover and an automated theorem-prover are utilised to formally verify a nonlinear attitude control system of a generic multi-rotor UAV over a stability domain within the dynamical state space of the drone. Further benefits of the procedures are that some of the resulting methods can be implemented onboard the aircraft to detect when its controller breaches its flight envelope limits due to severe weather conditions or actuator/sensor malfunction. Such a detection procedure can be used to advise the remote pilot, or an onboard intelligent agent, to decide on some alterations of the planned flight path or to perform emergency landing.