Perception-based Quantitative Runtime Verification for Learning-enabled Cyber-Physical Systems

This paper proposes a perception-based quantitative approach to verify the safety of learning-enabled Cyber-Physical Systems (Le-CPS) at runtime. The proposed approach is developed based on probstar reachability, a new quantitative verification method for deep neural networks. It has two main components: perception-based runtime modeling and runtime quantitative verification. The perception-based runtime modeling method uses a probabilistic perception network to estimate the poses (modeled as a multivariate normal distribution) of moving obstacles. We transform sensing, actuating, and perception uncertainties into probabilistic initial conditions for the system's states. The system model and initial conditions serve as inputs to a runtime reachability analysis algorithm, which constructs the system's reachable sets for a short future horizon. These reachable sets are then used to quantitatively verify the system's safety violation probability in real time. Our approach has been successfully deployed and validated on a real learning-based F1Tenth testbed with multiple autonomous driving scenarios, demonstrating its potential for enhancing the safety and reliability of autonomous systems. The reachable sets are used to quantitatively verify the system's safety violation probability at runtime.