CAREER: A Data-Driven Approach for Verification and Control of Cyber-Physical Systems

CAREER项目通过采用控制理论、计算机科学和运筹学的思想，为具有未知封闭模型的复杂网络物理系统（CPS）开发正式验证和控制器综合方案。此类系统的新兴例子包括自动驾驶汽车、自动运输网络、智能电网和集成医疗设备。该项目的主要新颖之处在于绕过模型识别阶段，仅使用从其行为中收集的数据直接验证或综合CPS的控制软件，以满足复杂的安全要求。本项目还严格量化了对验证结果或综合控制软件正确性的置信度保证，并可根据数据量进行改进。不幸的是，给定可接受的置信度，所需的数据数量会随着系统的大小而迅速增长。这就是所谓的样本复杂度。为了解决这个问题，特别是对于大规模的CPS，该项目最终提出了一种分而治之的策略，将数据驱动的验证或控制器合成问题分解为半独立的问题，其中解决每个子问题需要的数据量要小得多。该项目的研究成果将有助于PI的长期教育计划：i)以“端到端观点”开发CPS的统一课程，从控制和离散系统理论的基础开始，转向硬件/软件实现；Ii)通过本项目开发的平台和基准，为这些课程带来实践学习；iii)最后，通过利用科罗拉多大学博尔德分校的外展项目，招募第一代和代表性不足的工程专业学生，并让他们参与本项目使用的平台，提高本科生的保留率。该项目提出了一种可扩展的数据驱动方法，用于具有未知模型（又名黑箱系统）的CPS控制软件的形式化验证和综合。为此，给定CPS的时间逻辑要求（例如，那些表示为线性时间逻辑公式的要求），它们将根据表示它们的自动机的结构分解为更简单的任务。然后，通过使用从系统中收集的数据构建所谓的屏障函数来解决那些更简单的任务。特别地，对于这些简单任务，障函数上的条件首先被表述为鲁棒凸规划（RCP），它在技术上是半无限线性规划。由于模型未知，直接求解这些RCP是不容易处理的。相反，该项目考虑从系统收集的一组数据，并解决场景凸规划（SCP），这是有限的线性规划。将通过求解SCP得到的屏障函数组合起来，以验证给定的需求或提供执行该需求的控制器。该项目还对验证结果或合成控制器的正确性严格量化置信度（即样本外性能保证）。为了解决大规模CPS的潜在样本复杂性，该项目通过利用系统中存在的自然结构，提出了自适应采样和模块化数据驱动方案。最后，所提出的算法将被实施到开源软件工具中，以自动化所提出的数据驱动技术，并在人工胰腺系统和一个比例模型自动驾驶汽车团队上进行评估。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

This CAREER project develops formal verification and controller synthesis schemes for complex cyber-physical systems (CPS) with unknown closed-form models by embracing ideas from control theory, computer science, and operations research. Emerging examples of such systems include autonomous cars, autonomous transportation networks, smart grids, and integrated medical devices. The main novelty of this project lies in bypassing the model identification phase and directly verifying or synthesizing control software for CPS against complex safety requirements using just data collected from their behaviors. This project also quantifies rigorously a confidence guarantee on the verification outcomes or the correctness of synthesized control software, which can be improved based on the amount of data. Given an acceptable confidence, unfortunately, the required number of data grows rapidly with the size of the system. This is known as the sample complexity. To tackle this issue, particularly, for large-scale CPS, the project finally proposes a divide and conquer strategy by breaking the data-driven verification or controller synthesis problems into semi-independent ones, where solving each subproblem requires a much smaller amount of data. The research outcomes of this project will contribute to the long term education plan of the PI by i) developing unified courses on CPS with an “end-to-end view,” starting from the foundations of control and discrete systems theory and moving to hardware/software implementations; ii) bringing hands-on learning to those courses by the platforms and benchmarks developed in this project; and iii) finally, improving undergraduate retention rates by leveraging the outreach programs at the University of Colorado Boulder to recruit first generation and underrepresented engineering students and engage them in the platforms used in this project.This project proposes a scalable data-driven approach for formal verification and synthesis of control software for CPS with unknown models (a.k.a. black-box systems). To do so, given temporal logic requirements (e.g., those expressed as linear temporal logic formulae) for CPS, they will be decomposed into simpler tasks based on the structures of automata representing them. Then, those simpler tasks are tackled by constructing so-called barrier functions using data collected from the systems. Particularly, the conditions over barrier functions for those simpler tasks are first formulated as robust convex programs (RCP) which are technically semi-infinite linear programs. Solving those RCP directly are not tractable due to unknown models. Instead, this project considers a set of data collected from the system and solves scenario convex programs (SCP), which are finite linear programs. Barrier functions resulted by solving SCP are combined to verify the given requirement or to provide a controller enforcing it. The project also quantifies rigorously a confidence (a.k.a. out-of-sample performance guarantee) on the verification outcomes or the correctness of synthesized controllers. To tackle the underlying sample complexity for large-scale CPS, this project proposes an adaptive sampling and a modular data-driven schemes by exploiting the natural structure present in the system. Finally, the proposed algorithms will be implemented into open-source software tools to automate the proposed data-driven techniques and evaluated on Artificial Pancreas systems and a team of scale-model autonomous vehicles.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.