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

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

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.