Verification Framework for Control System Functionality of Unmanned Aerial Vehicles

TL;DR

This paper introduces a formal verification framework for UAV control systems using theorem proving to ensure safety and robustness, with potential onboard implementation for real-time fault detection and flight safety.

Contribution

It presents a novel formal verification procedure for UAV control systems using theorem proving, enabling correctness checks and onboard fault detection capabilities.

Findings

Verified nonlinear attitude control system within stability domain

Demonstrated potential for onboard fault detection and safety assurance

Formal methods improve reliability of UAV control systems

Abstract

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 proceedures, a higher-order logic interactive theorem-prover and an automated theorem-prover are utilized 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 proceedures are that some of the resulting methods can be implemented onboard the aircraft to detect when its controller breaches its flight envelop 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.