Formal Analysis of Unmanned Aerial Vehicles Using Higher-Order-Logic Theorem Proving

What is it about?

The continuous dynamics of Unmanned Aerial Vehicles (UAVs) are generally modeled as a set of differential equations. In this paper, we propose to use higher-order-logic theorem proving for formally analyzing the continuous dynamics of UAVs. In particular, we provide a formalization of the navigation and aircraft's body-fixed frames and their associated transformations. We also provide formal reasoning support for analyzing the Multiple-input Multiple-output (MIMO) systems, which are in turn used for formally analyzing the continuous dynamics of UAVs using HOL Light. For illustration, we use our proposed framework for the formal stability analysis of the CropCam UAV using HOL Light.

Featured Image