Bounded Verification of Adaptive Flight Control Systems

Abstract

We formally verify a direct model reference adaptive control (MRAC) method that is used to enable flight control in adverse conditions. We use the bounded verification approach and verify the system by introducing templates for both the assumptions and the guarantees, and using the tool QEPCAD to solve the resulting exists-for-all formula. We also present results from an analysis performed on indirect and hybrid adaptive flight controllers.