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

CPS：协同：协作研究：实时智能嵌入式系统（SORTIES）优化的语义

• 批准号: 1619729
• 负责人: Behcet Acikmese
• 金额: $ 20.23万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-01-01 至 2019-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1619729&HistoricalAwards=false
• 关键词: CPS; Synergy; Collaborative; Research; Semantics

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.

技术的进步意味着，当前仍需要人类操作员的计算机控制的物理设备，例如汽车，火车，飞机和医疗系统，可以完全自主运行，并自行做出合理的决定。自动驾驶汽车和无人机是这个梦想的具体和高度宣传的面孔。 在实现这一梦想之前，我们必须解决对安全的需求 - 保证没有自主权出现的不良行为。高度宣传的技术事故，例如火箭发射故障，治疗期间不受控制的辐射暴露，飞机自动化故障和意想不到的汽车加速，这是警告说，如果在此类网络物理系统的设计中没有充分解决安全性，可能会发生的情况。 安全分析的一种方法是使用适用正式逻辑的软件工具来证明系统控制软件中没有不希望的行为。 在先前的工作中，这种方法被证明可用于简单控制器软件，该软件是由Simulink图（例如Simulink图）的工具自动生成的。 但是，自主决策需要更复杂的软件，该软件能够实时解决优化问题。包括此类优化算法的控制软件的正式验证仍然是一个未满足的挑战。项目排序（实时智能嵌入式系统的优化语义）借鉴了优化理论，控制理论和计算机科学方面的专业知识，以应对这一挑战。从凸优化算法的收敛性属性开始，Sorties研究了如何将这些属性自动表示为归纳不变的算法，以实现算法的软件，然后将这些属性与源代码本身结合在一起，作为正式注释中的源代码中，这些属性将基础推理传达给软件工程师和现有的计算机所为计算机所涉及的计算机所提供的验证工具。 排序目标是一种开源 - 仪式的自动编码器，它采用优化算法及其收敛属性作为输入，并产生带注释的，可验证的代码作为输出。该工具在几个示例中的演示，例如火星着陆器，飞机航空电子系统和喷气发动机控制器，表明注释产生的质量证据与其在真正功能性产品中的应用完全兼容。 项目研究通过培训“三语”专业人员的培训来融入教育，他们在系统操作，程序分析以及控制和优化理论方面同样熟悉。