New Search

Export article

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

Sa’Ed Abed, Adnan Rashid, Osman Hasan

Abstract: The continuous dynamics of unmanned aerial vehicles (UAVs) are generally modeled as a set of differential equations. Traditionally, these continuous dynamics of UAVs are analyzed using paper-and-pencil proof and computer-based testing or simulations to study the performance, stability, and various other control characteristics of the aircraft flying in the air. However, these techniques suffer from their inherent limitations such as human error proneness, sampling-based analysis, approximations of the mathematical results, and the usage of unverified algorithms. Thus, these methods cannot be trusted when considering the utility of UAVs in many safety-critical applications. To overcome the limitations of the aforementioned techniques, it is proposed to use higher-order-logic theorem proving for formally analyzing the continuous dynamics of UAVs. In particular, a formalization of complex-valued matrices in higher-order logic is provided using the HOL Light theorem prover, which is in turn used for the formalization of the navigation’s and aircraft’s body-fixed frames, as well as their associated transformations. Formal reasoning support is also provided for analyzing the multiple-input multiple-output 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.
Keywords: safety / Differential / Formalization / Hol / modeled / theorem / continuous dynamics of UAVs

Scifeed alert for new publications

Never miss any articles matching your research from any publisher
  • Get alerts for new papers matching your research
  • Find out the new papers from selected authors
  • Updated daily for 49'000+ journals and 6000+ publishers
  • Define your Scifeed now

Share this article

Click here to see the statistics on "Journal of Aerospace Information Systems" .
References (21)
    Back to Top Top