Towards flight control verification using automated theorem proving

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.