CAREER: Provably Correct Control Software for Autonomous High-Performance Agents

点击翻译按钮获取中文摘要

The research objective of this Faculty Early Career Development (CAREER) Program award is to investigate a rigorous approach to control software certification for multi-task agents with complex dynamics. The analysis tools stem from a novel treatment of integral quadratic constraint (IQC) based uncertainty analysis, and can handle hybrid non-stationary parameter-dependent control systems and a wide range of uncertainties. These tools provide, at the algorithmic level, a sophisticated method for validation of control systems by determining ellipsoids that are invariant under task-based state transitions. The same analysis tools will be utilized to generate annotated control program code based on the Floyd-Hoare paradigm, migrating in the process high-level, systemic properties down to the executable code. The annotated code can then be checked for correctness by using a theorem prover augmented with appropriate theories. Modules stemming from the IQC-based analysis will be introduced into existing, public domain autocoders to enable high-level annotations with properties. The approach will be implemented on an uninhabited aerial vehicle (UAV) platform. If successful, the research will apply to complex high-performance systems such as UAVs operating autonomously in dynamic environments and sharing space with humans and human-piloted vehicles. The formal validation approach can be applied before the physical prototype is tested or even built, promising reductions in time and cost of the software development process and an expedited transition of technology to practice. This formal validation also leads to formal safety guarantees, tackling one of the critical barriers to the integration of autonomous vehicles into civil society. The integration of research and education will be achieved through the UAV testbed, which will be utilized to construct educational modules and provide a hands-on environment for courses and undergraduate research. The educational modules will be communicated to pre-college students, including women and minorities, through outreach activities.