Formal Methods for the Design and Verification of UAV Feedback Controls

This thesis is concerned with using formal methods to develop new verification schemes for UAVs control systems. Until now, control theories have been proved and verified manually by control scientists and engineers. Some computations of multivariable control systems, which include numerical bounds on modelling errors and state constraints, are difficult to check and verify manually by an engineer due to their complexity. In these cases, errors made by manual derivation can be dangerous for safe especially for safety-critical system such as unmanned aerial vehicles. To mitigate these issues, this thesis presents examples of formal proofs of theoretical control theorems. These represent the first steps towards verifying control theories by software using formal methods by interactive theorem proving. The thesis presents a new nonlinear controller for unmanned aerial vehicles by jointly addressing modelling uncertainty and external disturbances. The verification framework which developed in this thesis is promising and may encourage the use of such methods in control system verification of safety-critical systems in general. The symbolic methods are generic and potentially generalise to verification of a variety of industrial control systems, where performance loss is damaging and therefore analysis is important to be carried out formally.