PhD Defense by Corbin Klett

Event Details
  • Date/Time:
    • Thursday December 23, 2021
      10:00 am - 12:00 pm
  • Location: TSRB 423
  • Phone:
  • URL: Bluejeans
  • Email:
  • Fee(s):
  • Extras:
No contact information submitted.

Summary Sentence: Towards Tractable Methods for Formal Verification of Autonomy in Aerospace Systems

Full Summary: No summary paragraph submitted.

Corbin Klett

(Advisor: Eric Feron)


will defend a doctoral thesis entitled


Towards Tractable Methods for Formal Verification of

Autonomy in Aerospace Systems




Thursday, December 23rd at 10am

TSRB 423



Formal verification techniques for control systems are developed and applied to real-world aerospace systems, including experimental platforms as well as mathematical models which contain features that closely resemble those found in real systems. Though prolific in academia, these analysis techniques are not prevalent in industry, where system-level requirements are commonly validated by rudimentary measures of system robustness such as gain and phase margin as well as by extensive simulation and testing. Conventional methods have proven their efficacy for the certification of safety-critical systems but are also incapable of exhaustively testing a system's behaviors. Integrating more advanced mathematical techniques into system design and analysis workflows could enable additional autonomy capabilities, improve safety, and decrease development and certification costs.


The verification strategies developed and demonstrated in this work rely on key results from nonlinear systems theory, real algebraic geometry, and convex optimization. First, a method for constructing homogeneous polynomial Lyapunov functions is presented for the class of nonlinear systems which can be represented by a linear time-varying or a switched-linear system. Procedures are developed that produce improved certificates of set invariance, bounds on peak norms, and system stability margin. Additionally, an algorithm that uses a Lyapunov function certificate to search for a worst-case trajectory is developed and applied to several aerospace examples, including an attitude-controlled spacecraft. Characterization of the safe operating envelope for this spacecraft is demonstrated with Lyapunov techniques. This result is integrated into a run-time assurance algorithm, which is shown to significantly increase the vehicle's operational capabilities as demonstrated on an experimental hardware platform. Finally, strategies are proposed for the formal analysis of gas turbine engine control systems which offer advantages over some conventional practices.



  • Prof. Eric Feron – Aerospace Engineering
  • Prof. Yongxin Chen – Aerospace Engineering
  • Prof. Kyriakos Vamvoudakis – Aerospace Engineering
  • Prof. Sam Coogan – Electrical and Computer Engineering, Civil and Environmental Engineering
  • Prof. Panos Tsiotras – Aerospace Engineering

Additional Information

In Campus Calendar

Graduate Studies

Invited Audience
Faculty/Staff, Public, Undergraduate students
Phd Defense
  • Created By: Tatianna Richardson
  • Workflow Status: Published
  • Created On: Dec 16, 2021 - 12:45pm
  • Last Updated: Dec 16, 2021 - 12:45pm