Runtime Verification of Autonomous Driving Systems in CARLA

Abstract

Urban driving simulators, such as CARLA, provide 3-D environments and useful tools to easily simulate sensorimotor control systems in scenarios with complex multi-agent dynamics. This enables the design exploration at the early system development stages, reducing high infrastructure costs and high risks. However, due to the high-dimensional input and state spaces of closed-loop autonomous driving systems, their testing and verification is very challenging and it has not yet taken advantage of the recent developments in theory and tools for runtime verification. We show here how to integrate the recently introduced (Formula Presented) library, for runtime verification of STL (Signal Temporal Logic) specifications, with the CARLA simulator. Finally, we also present the obtained results from monitoring quantitatively interesting requirements for an experimental Adaptive Cruise Control system tested in CARLA.