Abstract
AI-powered Cyber-Physical Systems (CPS) form the basis of emerging and future smart services, improve quality of life, and bring advances in many critical areas, including intelligent transportation, robotics, smart cities and smart healthcare. The development of faster and more reliable networks accelerates the integration of Cyber-Physical Systems (i-CPS). A central problem is how to build reliable i-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 conduct large-scale data-driven analytic for i-CPS, including the first study on over 1000 city requirements and study on uncertainty in i-CPS. Secondly, we develop the first decision support system for conflict detection and resolution for smart cities, which significantly improves cities' safety and performance in our experiments and simulation. Thirdly, we create novel formal specification languages and efficient runtime verification techniques for large-scale i-CPS with theoretical guarantees. The new specification languages achieve over 95% expressiveness coverage on real-world city requirements, while state-of-the-art only have 43% coverage. Additionally, we build a runtime monitoring tool to support specifying and monitoring requirements by different stakeholders in i-CPS. Fourthly, 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. The framework is general to be applied to various deep sequential prediction models for i-CPS and significantly outperforms state-of-the-art. At last, we develop the first approach for calibrating the uncertainty estimation in Bayesian Recurrent Neural Networks (RNNs) through predictive monitoring with critical system requirements. It achieves a much higher quality of uncertainty estimation comparing to the baseline approaches.
