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

本学院早期职业发展（Career）计划奖的研究目标是研究一种严格的方法来控制具有复杂动态的多任务代理的软件认证。该分析工具源于基于积分二次约束（IQC）的不确定性分析的新处理，可以处理混合非平稳参数依赖控制系统和大范围的不确定性。这些工具在算法层面上提供了一种复杂的方法，通过确定在基于任务的状态转换下不变的椭球来验证控制系统。同样的分析工具将被用来生成基于Floyd-Hoare范式的带注释的控制程序代码，将过程中的高级系统属性迁移到可执行代码中。然后可以使用添加了适当理论的定理证明器来检查带注释的代码的正确性。源自基于iqc的分析的模块将被引入到现有的公共领域自动编码器中，以支持带有属性的高级注释。该方法将在无人飞行器（UAV）平台上实施。如果成功，该研究将适用于在动态环境中自主操作的无人机，以及与人类和人类驾驶车辆共享空间等复杂的高性能系统。正式的验证方法可以在物理原型测试甚至构建之前应用，这有望减少软件开发过程的时间和成本，并加速技术向实践的过渡。这种正式的验证也会带来正式的安全保证，解决了自动驾驶汽车融入公民社会的一个关键障碍。将通过无人机试验台实现科研与教育的整合，该试验台将用于构建教育模块，并为课程和本科生研究提供实践环境。将通过外联活动向包括妇女和少数民族在内的大学预科学生宣传这些教育模块。

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.