CSR: Small: Model Exploration for Cyber-Physical Systems

信息物理系统（CPS）紧密结合计算和通信来控制物理系统。计算机控制系统的例子包括医疗设备、飞机和汽车。这类系统过于复杂，设计师无法完全理解其行为的每个细节。另一方面，了解此类系统的高级特性至关重要，因为大多数系统都对安全至关重要。该项目旨在从两个不同的方向改进控制系统的模型探索技术。首先，它研究了部分指定系统属性的形式语言。我们的目标是使这些规范更加具体，以一种能够精确地演示系统所满足的属性的方式。其次，研究了时间逻辑修正问题。也就是说，如果自动分析显示期望的系统规格不能被满足，那么工具如何提出一个可以被满足并且尽可能接近最初预期的替代规格呢？该研究项目将采用和适应从时间逻辑查询，空性和覆盖到CPS设置的想法。该项目的预期结果包括用于(i)基于模型的控制系统探索和（ii）控制系统综合工具调试的工具。因此，开发的技术将随时可供嵌入式控制系统的设计人员使用，以帮助他们探索和更好地了解他们的系统。此外，这项研究的实践和理论结果将通过PI教授的一些高级课程和研讨会传播给本科生和研究生以及当地工业的工程师。

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.