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.