To ensure that an aircraft is safe to fly, a complex, lengthy and costly process must be undertaken. Current aircraft control systems verification methodologies are based on conducting extensive simulations in an attempt to cover all worst-case scenarios. A Nichols plot is a technique that can be used to conclusively determine if a control system is stable. However, to guarantee stability within a certain margin of uncertainty requires an informal visual inspection of many plots. To leverage the safety verification problem, we present in this paper a method for performing a formal Nichols Plot analysis using the MetiTarski automated theorem prover. First the transfer function for the flight control system is extracted from a Matlab/Simulink design. Next, using the conditions for a stable dynamical system, an exclusion region of the Nichols Plot is defined. MetiTarski is then used to prove that the exclusion region is never entered. We present a case study of the proposed approach applied to the lateral autopilot of a Model 24 Learjet. © 2011 Springer-Verlag.
CITATION STYLE
Denman, W., Zaki, M. H., Tahar, S., & Rodrigues, L. (2011). Towards flight control verification using automated theorem proving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6617 LNCS, pp. 89–100). https://doi.org/10.1007/978-3-642-20398-5_8
Mendeley helps you to discover research relevant for your work.