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）将计算和通信紧密结合起来，以控制物理系统。 计算机控制系统的例子包括医疗设备、飞机和汽车。 这样的系统太复杂了，设计者无法完全理解它们的每一个细节。 另一方面，了解这些系统的高级属性是至关重要的，因为大多数是安全critical.This项目旨在提高控制系统在两个不同的方向模型探索技术。 首先，它研究了部分指定系统属性的形式语言。 我们的目标是使这些规范更加具体，以某种方式，他们证明了什么是系统所满足的属性。其次，研究了时态逻辑的修改问题。 也就是说，如果自动分析表明，所需的系统规范不能得到满足，工具如何提出一个替代规范，可以满足，并尽可能接近原来的意图？ 该研究项目将采用和适应的想法，从时序逻辑查询，真空和覆盖CPS设置。该项目的预期成果包括工具（i）控制系统的模型为基础的探索和（ii）控制系统综合工具的调试。 因此，开发的技术将随时提供给嵌入式控制系统的设计人员，以帮助他们探索和更好地理解他们的系统。此外，这项研究的实践和理论成果将通过PI教授的一些高级课程和研讨会传播给本科生和研究生以及当地行业的工程师。