CPS: Synergy: Physically-Informed Assertions for CPS Development and Debugging

这个项目的目标是实现断言驱动的开发和调试网络物理系统(CP)，其中所需的条件作为设计的一部分被形式化。与软件工程中断言的传统使用不同，CPS要求网络与物理的紧密耦合，包括在系统验证中。该项目使用关键物理属性的数学模型来指导断言的创建，识别不一致或不可行的断言，并定位CPS失败的潜在原因。其目标是产生使用物理模型来指导基于断言的网络物理系统验证的方法和工具。正在开发一种断言语言，它建立在数理逻辑的基础上，同时提供常用编程语言的熟悉性。这一基础为CP启用了新的自动化调试技术。通过利用编码物理定律的模型和自动决策程序，正在开发的技术通过区分不一致或不可行的物理状态和有效的物理状态来帮助识别CPS失败的原因。这一基于模型的方法结合了使用概率和非概率测量来评估这些物理状态的方法。两个安全关键应用指导研究并展示了对CPS开发的影响：自动车辆的协调控制和左心室辅助装置(LVAD)的监测和控制。对这些安全关键型应用的关注是对招收和教育工程专业学生的激励，这些学生对如何通过计算进步实现自己的生活抱有很高的期望。此外，这项研究还提出了验证安全和有效的CPS所需的方法，提高了公众对其应用于安全关键系统的信心。

This project's objective is to enable assertion-driven development and debugging of cyber-physical systems (CPS), in which required conditions are formalized as part of the design. In contrast with traditional uses of assertions in software engineering, CPS demand a tight coupling of the cyber with the physical, including in system validation. This project uses mathematical models of key physical attributes to guide creation of assertions, to identify inconsistent or infeasible assertions, and to localize potential causes for CPS failures. The goal is to produce methods and tools that use physical models to guide assertion-based verification of cyber-physical systems.An assertion language is being developed that is founded in mathematical logic while providing the familiarity of commonly used programming languages. This foundation enables new automated debugging techniques for CPS. By leveraging models that encode laws of physics and an automated decision procedure, the techniques being developed help identify causes of CPS failures by distinguishing inconsistent or infeasible physical states from valid ones. This model-based approach incorporates means to assess these physical states using both probabilistic and non-probabilistic measures.Two safety-critical applications guide the research and demonstrate the impact on the development of CPS: coordinated control of autonomous vehicles and monitoring and control of left-ventricular assist devices (LVADs). The focus on these safety-critical applications are motivational for recruiting and educating engineering students who have high expectations for how their lives should be enabled by computing advances. Further, this research advances methods needed to validate safe and effective CPS, promoting the public's confidence in their application to safety-critical systems.