Using an Interactive Theorem Prover for Formally Analyzing the Dynamics of the Unmanned Aerial Vehicles
Mobile Robot: Motion Control and Path Planning, Ch. 9, Studies in Computational Intelligence, Vol. 1090, Springer, pp. 253–282
Theorem Proving · HOL Light
Formalizing complex-valued matrices and MIMO reasoning support in HOL Light to formally analyze the continuous dynamics and stability of unmanned aerial vehicles.
Abstract
The continuous dynamics of Unmanned Aerial Vehicles (UAVs) are generally modeled as a set of differential equations, traditionally analyzed using paper-and-pencil proofs and computer-based testing or simulation. These techniques suffer from human error-proneness, sampling-based analysis, mathematical approximations, and unverified algorithms — limitations that cannot be trusted given the safety-critical applications of UAVs.
We propose higher-order-logic theorem proving to formally analyze UAV continuous dynamics: formalizing complex-valued matrices in HOL Light, which in turn supports the formalization of navigation and aircraft body-fixed frames and their transformations, and reasoning about Multiple-Input Multiple-Output (MIMO) systems. We illustrate the framework with the formal stability analysis of the CropCam UAV.
Framework
People
Related Publications