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.