CAREER: High-Assurance Design of Learning-Enabled Cyber-Physical Systems with Deep Contracts

Next-generation cyber-physical systems (CPS) will increasingly rely on machine learning algorithms for situational awareness and decision-making, with the promise of enhancing human capabilities. Examples range from autonomous vehicles and robots to computer-controlled factory lines and wearable medical devices. However, learning-enabled systems have shown to be very sensitive to training data and have difficulty in ensuring functional safety and robustness. The undesired outcomes of recent deployments, such as the accidents involving semi-autonomous vehicles, raise questions about the design principles needed to build learning-enabled systems that are safe. This project aims to develop the foundations of a novel methodology for the design and verification of learning-enabled CPS. It will pursue a compositional framework and computational tools that can reason about the uncertainty and approximation introduced by learning components and enable system design via a hierarchical and modular approach. The proposed research can have a highly positive influence on the design and real-world deployment of safe and cost-effective autonomous systems for a variety of applications, including autonomous driving, robotics, and industrial automation. Moreover, it has the potential to offer a unifying framework for reasoning about a number of robust and fault-tolerant design approaches that are currently based mostly on ad hoc solutions. Collaborations with industry partners will be pursued to facilitate transitioning the research findings into practice. An educational plan including new undergraduate and graduate courses and a program for pre-college students will complement the research effort, aiming to educate the next generation of engineers and researchers on the concepts and the multidisciplinary attitude needed to realize "intelligent" systems that are safe, technologically and economically feasible, and seamlessly interacting with people. The project develops a compositional framework for reasoning about the probabilistic behaviors of CPS built out of unreliable components. The framework relies on stochastic models of the interfaces between the components and their environments, termed deep contracts, together with rigorous rules for composing and refining them. Rich, quantitative, logic-based stochastic specification formalisms and data-driven modeling techniques will be leveraged to express and propagate computationally tractable representations of uncertainty at different abstraction levels. The framework will be vertically-integrated and offer mapping mechanisms to bridge heterogeneous models and heterogeneous decomposition architectures in the design hierarchy. It will provide computational tools to efficiently solve verification and synthesis problems with stochastic contracts. Finally, it will offer mechanisms to monitor requirements throughout the entire system life-cycle and provide assurance both at design time and runtime. 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.