Runtime Verified Neural Networks for Cyber-Physical Systems

There is increasing use of artificial neural networks in Cyber-Physical Systems (CPS) such as autonomous vehicles (AVs). Here, convolutional neural networks (CNNs) are widely used for different types of computer-vision tasks. The complex nature of the CNN makes verification of CNN-based CPS extremely difficult. Through this work, we propose a formal runtime verification (RV) approach that employs user-specified policies constructed through Valued Discrete Timed Automata (VDTA). This innovative approach serves as a powerful tool for ensuring the adherence of the system to predefined safety-critical policies, providing a formalized method to handle the complexities of CNNs in safety-critical contexts by treating them as black boxes. To demonstrate the effectiveness of this runtime verification approach, we model a CNN-based AV that is embedded with a runtime monitor. The different control units of the AV are trained using RL-based Q-Learning technique and integrate them into some of its key components. We also analyse how increase in the number of properties to be monitored affects the execution time of the overall system.