Verification framework for control theory of aircraft
Open Access
- 10 May 2022
- journal article
- research article
- Published by Cambridge University Press (CUP) in The Aeronautical Journal
- Vol. 127 (1307), 41-56
- https://doi.org/10.1017/aer.2022.45
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 procedures, a higher-order logic interactive theorem-prover and an automated theorem-prover are utilised 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 procedures are that some of the resulting methods can be implemented onboard the aircraft to detect when its controller breaches its flight envelope 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.Keywords
This publication has 25 references indexed in Scilit:
- Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems (Invited Lecture)Lecture Notes in Computer Science, 2015
- Automated Real Proving in PVS via MetiTarskiLecture Notes in Computer Science, 2014
- Formal Analysis of Steady State Errors in Feedback Control Systems Using HOL-LightPublished by EDAA ,2013
- MetiTarski: Past and FutureLecture Notes in Computer Science, 2012
- Speech Outcomes after Tonsillectomy in Patients with Known Velopharyngeal InsufficiencyInternational Journal of Otolaryngology, 2011
- Differential Dynamic Logic for Hybrid SystemsJournal of Automated Reasoning, 2008
- Z3: An Efficient SMT SolverLecture Notes in Computer Science, 2008
- QEPCAD BACM SIGSAM Bulletin, 2003
- Hoare Logics in Isabelle/HOLPublished by Springer Science and Business Media LLC ,2002
- A theory of type polymorphism in programmingJournal of Computer and System Sciences, 1978