Formal Methods Enhanced Deep Learning for Integrated Cyber-Physical Systems
AI-powered integrated Cyber-Physical Systems (i-CPS) form the basis of emerging and future smart services, improve quality of life, and bring advances in many critical areas, including smart cities and health care. A central problem is how to build reliable AI-CPS facing significant new challenges due to the increasing integration, complexity, and environmental uncertainties. Targeting these challenges, in this dissertation, we develop rigorous and robust models for reliable i-CPS by integrating formal methods and deep learning with the following main contributions. First, we identify conflicts in large-scale i-CPS and formalize i-CPS safety and performance requirements using Signal Temporal Logic (STL). We develop a decision support system for conflict detection and resolution among integrated IoT services in i-CPS through model-driven and data-driven prediction models and runtime verification. Secondly, we create novel formal specification languages and efficient runtime verification techniques for large-scale i-CPS with theoretical guarantees. To tackle the limitation of existing formal logic, we develop SaSTL---a novel Spatial Aggregation Signal Temporal Logic (SaSTL)---for the efficient runtime monitoring of safety and performance requirements. The new specification languages achieve over 95% expressiveness coverage on real-world city requirements. Additionally, we build a SaSTL-based monitoring tool to support different stakeholders' decision-making to specify and runtime monitor their requirements in smart cities. Thirdly, we develop novel formal methods enhanced deep learning techniques to increase the robustness of sequential prediction by incorporating formal specification and verification into the learning process. We develop a new temporal logic-based learning framework, STLnet, which guides the RNN learning process with auxiliary knowledge of model properties and produces a more robust model for improved future predictions. We also show the generalizability of these techniques for various neural networks and applications. Fourthly, we develop a novel approach for monitoring sequential predictions generated from Bayesian Recurrent Neural Networks that can capture the inherent uncertainty in CPS, drawing on insights from our study of real-world CPS datasets. We propose a new logic named Signal Temporal Logic with Uncertainty (STL-U) to monitor a flowpipe containing an infinite set of uncertain sequences predicted by Bayesian RNNs. Furthermore, we develop novel criteria that leverage STL-U monitoring results to calibrate the uncertainty estimation in Bayesian RNNs. Evaluation results on large-scale real-world city data show that our approaches significantly improve the accuracy and robustness of deep learning models and achieve well-calibrated uncertainty. Moreover, the system also effectively improves smart cities' safety and performance via smart city simulations. At last, we discuss the insights of this work and future research directions on further integrating formal methods and deep learning towards explainable, verifiable, and reliable AI-CPS addressing a broad spectrum of social and technical challenges.
- Haiying Shen, Committee Chair, (CS/SEAS/UVA)
- John Stankovic, Co-advisor, (CS/SEAS/UVA)
- Lu Feng, Co-advisor, (CS/SEAS/UVA)
- Aidong Zhang (CS/SEAS/UVA)
- John Lach (CS/SEAS/UVA, SEAS/GWU)