CSR: Small: Model Exploration for Cyber-Physical Systems

CSR：小：网络物理系统的模型探索

• 批准号: 1116136
• 负责人: Georgios Fainekos
• 金额: $ 37.5万
• 依托单位: Arizona State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-09-01 至 2015-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1116136&HistoricalAwards=false
• 关键词: CSR; Small; Model; Exploration; Cyber

Cyber-Physical Systems (CPS) tightly integrate computation and communication to control a physical system. Examples of computer-controlled systems include medical devices, airplanes, and automobiles. Such systems are too complex for the designers to completely understand their behavior in every detail. On the other hand, understanding the high-level properties of such systems is of paramount importance since most are safety-critical.This project seeks to improve model exploration techniques for control systems in two distinct directions. First, it investigates formal languages that partially specify the properties of a system. The goal is to make those specifications more concrete, in a way that they demonstrate what are precisely the properties satisfied by the system. Second, it studies the temporal logic revision problem. Namely, if automatic analysis shows that a desired system specification cannot be satisfied, how can tools propose an alternative specification which can be satisfied and is as close as possible to the originally intended one? The research project will adopt and adapt ideas from temporal logic queries, vacuity and coverage to the CPS setting.Expected results of the project include tools for (i) the model based exploration of control systems and (ii) the debugging of control system synthesis tools. As a result, the developed techniques will be readily available to designers of embedded control systems to help them explore and better understand their systems. Additionally, the practical and theoretical results of this research will be disseminated to undergraduate and graduate students as well as engineers in local industries through a number of advanced courses and seminars that the PI is teaching.

网络物理系统（CPS）紧密整合了计算和通信以控制物理系统。 计算机控制系统的示例包括医疗设备，飞机和汽车。 这样的系统太复杂了，对于设计人员来说，无法在每个细节上完全理解其行为。 另一方面，了解此类系统的高级特性至关重要，因为大多数是安全至关重要的。该项目旨在改善两个不同方向的控制系统的模型勘探技术。 首先，它研究了正式的语言，该语言部分指定了系统的属性。 目的是使这些规格更具体，以证明系统所满足的属性的方式。其次，它研究了时间逻辑修订问题。 也就是说，如果自动分析表明无法满足所需的系统规范，那么工具如何提出可以满足并尽可能接近原本打算的替代规范？ 研究项目将采用并适应时间逻辑查询，空缺和覆盖范围到CPS设置的想法。项目的预期包括（i）基于模型的控制系统探索的工具以及（ii）控制系统合成工具的调试。 结果，嵌入式控制系统的设计人员将很容易获得开发的技术，以帮助他们探索和更好地了解其系统。此外，这项研究的实际和理论结果将通过PI所教学的许多高级课程和研讨会传播给本科和研究生以及当地行业的工程师。