Formal Analysis of Unmanned Aerial Vehicles Using Higher-Order-Logic Theorem Proving
- 1 September 2020
- journal article
- research article
- Published by American Institute of Aeronautics and Astronautics (AIAA) in Journal of Aerospace Information Systems
- Vol. 17 (9), 481-495
- https://doi.org/10.2514/1.i010730
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
This publication has 23 references indexed in Scilit:
- R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial SystemsPublished by Springer Science and Business Media LLC ,2015
- A formal approach for identifying assurance deficits in unmanned aerial vehicle softwarePublished by Springer Science and Business Media LLC ,2015
- Hybrid Theorem Proving of Aerospace Systems: Applications and ChallengesJournal of Aerospace Information Systems, 2014
- Hierarchical hybrid modelling and control of an unmanned helicopterInternational Journal of Control, 2014
- The HOL Light Theory of Euclidean SpaceJournal of Automated Reasoning, 2012
- Model checking agent programming languagesAutomated Software Engineering, 2011
- Safety, Security, and Rescue Missions with an Unmanned Aerial Vehicle (UAV)Journal of Intelligent & Robotic Systems, 2011
- Formal Methods for the Certification of Autonomous Unmanned Aircraft SystemsLecture Notes in Computer Science, 2011
- A military perspective on small unmanned aerial vehiclesIEEE Instrumentation & Measurement Magazine, 2004
- Aircraft Trajectory Modeling and Alerting Algorithm VerificationLecture Notes in Computer Science, 2000