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

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

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.