CommonUppRoad: A Framework of Formal Modelling, Verifying, Learning, and Visualisation of Autonomous Vehicles

TL;DR

This paper introduces CommonUppRoad, a framework integrating CommonRoad and UPPAAL to enhance safety, verification, and visualization in autonomous vehicle systems through formal modeling and machine learning.

Contribution

It presents a novel framework combining CommonRoad and UPPAAL with automatic model conversion, enabling systematic safety analysis and visualization for autonomous vehicles.

Findings

Framework effectively models autonomous vehicle behavior.

Automatic conversion simplifies system design and verification.

Scalability limits identified with potential solutions discussed.

Abstract

Combining machine learning and formal methods (FMs) provides a possible solution to overcome the safety issue of autonomous driving (AD) vehicles. However, there are gaps to be bridged before this combination becomes practically applicable and useful. In an attempt to facilitate researchers in both FMs and AD areas, this paper proposes a framework that combines two well-known tools, namely CommonRoad and UPPAAL. On the one hand, CommonRoad can be enhanced by the rigorous semantics of models in UPPAAL, which enables a systematic and comprehensive understanding of the AD system's behaviour and thus strengthens the safety of the system. On the other hand, controllers synthesised by UPPAAL can be visualised by CommonRoad in real-world road networks, which facilitates AD vehicle designers greatly adopting formal models in system design. In this framework, we provide automatic model conversions between CommonRoad and UPPAAL. Therefore, users only need to program in Python and the framework takes care of the formal models, learning, and verification in the backend. We perform experiments to demonstrate the applicability of our framework in various AD scenarios, discuss the advantages of solving motion planning in our framework, and show the scalability limit and possible solutions.