CPS: Synergy: Collaborative Research: Semantics of Optimization for Real Time Intelligent Embedded Systems (SORTIES)

技术的进步意味着，目前仍需要人工操作的计算机控制的物理设备，如汽车、火车、飞机和医疗系统，可以完全自主地操作，并自行做出理性的决定。自动驾驶汽车和无人机是这个梦想的具体和高度宣传的面孔。在实现这一梦想之前，我们必须解决对安全的需求--保证不会出现来自自主的不良行为。火箭发射失败、治疗过程中不受控制地暴露于辐射、飞机自动化故障和意外的汽车加速等备受关注的技术事故，都是对在此类网络物理系统的设计中没有充分考虑安全问题可能会发生的情况的警告。安全分析的一种方法是使用应用形式逻辑的软件工具来证明系统的控制软件中没有不受欢迎的行为。在以前的工作中，这种方法被证明适用于简单的控制器软件，这些软件是由工具从抽象模型(如Simulink图)自动生成的。然而，自主决策需要更复杂的软件，能够实时解决优化问题。包含这种优化算法的控制软件的形式化验证仍然是一个尚未满足的挑战。该项目(实时智能嵌入式系统优化的语义)利用优化理论、控制理论和计算机科学的专业知识来应对这一挑战。本文从凸优化算法的收敛性质入手，研究了如何将这些性质自动表示为算法的软件实现的归纳不变量，然后将这些性质合并到源代码本身中，作为形式注释，将潜在的推理传达给软件工程师和现有的计算机辅助验证工具。Touties的目标是一个携带开源语义的自动编码器，它将优化算法及其收敛特性作为输入，并产生带注释的、可验证的代码作为输出。该工具在火星着陆器、飞机航空电子系统和喷气发动机控制器等几个例子上的演示表明，注释产生的质量证据与其对真正功能产品的应用完全兼容。通过培训“三语”专业人员，项目研究与教育相结合，这些专业人员同样精通系统操作、程序分析以及控制和优化理论。

Advances in technology mean that computer-controlled physical devices that currently still require human operators, such as automobiles, trains, airplanes, and medical treatment systems, could operate entirely autonomously and make rational decisions on their own. Autonomous cars and drones are a concrete and highly publicized face of this dream. Before this dream can be realized we must address the need for safety - the guaranteed absence of undesirable behaviors emerging from autonomy. Highly publicized technology accidents such as rocket launch failures, uncontrolled exposure to radiation during treatment, aircraft automation failures and unintended automotive accelerations serve as warnings of what can happen if safety is not adequately addressed in the design of such cyber-physical systems. One approach for safety analysis is the use of software tools that apply formal logic to prove the absence of undesired behavior in the control software of a system. In prior work, this approach this been proven to work for simple controller software that is generated automatically by tools from abstract models like Simulink diagrams. However, autonomous decision making requires more complex software that is able to solve optimization problems in real time. Formal verification of control software that includes such optimization algorithms remains an unmet challenge.The project SORTIES (Semantics of Optimization for Real Time Intelligent Embedded Systems) draws upon expertise in optimization theory, control theory, and computer science to address this challenge. Beginning with the convergence properties of convex optimization algorithms, SORTIES examines how these properties can be automatically expressed as inductive invariants for the software implementation of the algorithms, and then incorporates these properties inside the source code itself as formal annotations which convey the underlying reasoning to the software engineer and to existing computer-aided verification tools. The SORTIES goal is an open-source-semantics-carrying autocoder, which takes an optimization algorithm and its convergence properties as input, and produces annotated, verifiable code as output. The demonstration of the tool on several examples, such as a Mars lander, an aircraft avionics system, and a jet engine controller, shows that the evidence of quality produced by annotations is fully compatible with its application to truly functional products. Project research is integrated with education through training of "tri-lingual" professionals, who are equally conversant in system operation, program analysis, and the theory of control and optimization.