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

CPS：协同：CPS 开发和调试的物理信息断言

• 批准号: 1239498
• 负责人: Christine Julien
• 金额: $ 89.18万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2018-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1239498&HistoricalAwards=false
• 关键词: CPS; Synergy; Physically; Informed; Assertions

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.

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