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

CPS：小型：用于验证和综合网络物理系统的数值和符号技术

• 批准号: 1935724
• 负责人: Parasara Duggirala
• 金额: $ 38.6万
• 依托单位: University of North Carolina at Chapel Hill
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-01-01 至 2021-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1935724&HistoricalAwards=false
• 关键词: CPS; Small; Numerical; Symbolic; Techniques

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.

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

项目成果

Reachability of Black-Box Nonlinear Systems after Koopman Operator Linearization

• DOI: 10.1016/j.ifacol.2021.08.507
• 发表时间: 2021-05
• 期刊: ArXiv
• 作者: Stanley Bak;Sergiy Bogomolov;Parasara Sridhar Duggirala;Adam R. Gerlach;Kostiantyn Potomkin