CPS: Small: Numerical and Symbolic Techniques for Verification and Synthesis of Cyber-Physical Systems

下一代信息物理系统（CPS），如汽车系统，需要软件和物理世界之间的紧密集成，以满足不断增长的需求。此类网络物理系统的非预期行为可能导致财产损失或更糟糕的情况，因此应通过对CPS进行正式分析来避免。这种分析是具有挑战性的，因为用于推理物理世界的工具主要使用实分析和代数，而用于推理软件的工具使用离散数学和算法。CPS的形式化分析的传统方法主要使用代数，其不能随着变量数量的增加而很好地扩展。本项目通过弥合物理世界的代数属性和软件的算法基础之间的差距，探索一种新的算法框架，用于严格推理网络物理系统。本项目开发的技术将利用在物理世界中广泛观察到的叠加原理的属性。通过分析CPS的行为样本集，这些算法可以推断出所有可能行为的大子集的属性。该项目将安全验证技术扩展到具有输入和参数的线性系统，并为状态反馈控制器的安全违规提出了一个新的反例概念。研究人员探索了一种模拟引导的合成框架，用于合成满足安全性和活性规范的控制器。研究人员将把研究成果纳入本科和研究生课程，向学生介绍嵌入式系统和控制设计。此外，该项目开发的算法和软件将广泛传播。

Next generation Cyber-Physical Systems (CPS), such as automotive systems, require tight integration between the software and the physical world to satisfy the ever-increasing requirements. Unintended behaviors of such cyber-physical systems might lead to loss of property or worse scenarios and hence should be avoided by performing formal analysis of CPS. Such analysis is challenging as the tools for reasoning about the physical world primarily use real-analysis and algebra whereas the tools for reasoning about software uses discrete mathematics and algorithms. Traditional approaches for formal analysis of CPS primarily use algebra, which do not scale well with the increase in the number of variables. This project explores a new algorithmic framework for rigorously reasoning about cyber-physical systems by bridging the gap between the algebraic properties of the physical world and algorithmic foundations of the software.The techniques developed in this project will exploit the property of superposition principle that is widely observed in the physical world. By analyzing a sample set of behaviors of CPS, these algorithms can infer properties of a large subset of all possible behaviors. The project extends safety verification techniques to linear systems with inputs and parameters, and develops a new notion of counterexample for safety violations of state feedback controllers. The investigators explore a simulation-guided synthesis framework for synthesizing a controller that meets both safety and liveness specifications. The investigator will incorporate research results into undergraduate and graduate classes to introduce students to embedded systems and control design. Additionally, the algorithms and software developed in this project will be disseminated broadly.