*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
Corbin Klett
(Advisor: Eric Feron)
will defend a doctoral thesis entitled
Towards Tractable Methods for Formal Verification of
Autonomy in Aerospace Systems
on
Thursday, December 23rd at 10am
TSRB 423
https://bluejeans.com/343850193/7366
Abstract
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.
Committee
