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

TL;DR

CommonUppRoad bridges formal methods and autonomous driving by enabling automatic conversion between CommonRoad scenarios and UPPAAL timed games, then supports learning- and verification-based motion planning within a Python-centric workflow. It introduces TG templates for vehicle dynamics and collision/offroad checks, and provides bidirectional strategy flows: UPPAAL strategies can become Python decision trees or trajectory injections into CommonRoad. The framework demonstrates usability and scalability through experiments, highlights the complementary strengths of search-based safety guarantees and learning-based optimization, and discusses compositional planning as a path to improved scalability. The work advances practical safety guarantees for AD by uniting formal verification, RL, and rich realistic scenarios, with direct visualization and integration into design workflows.

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.

Figures (5)

• Figure 1: Running example.
• Figure 2: Overall description of model conversion. Blue boxes are entities in CommonRoad. Green boxes are entities in UPPAAL.
• Figure 3: UPPAAL Models
• Figure 4: Scenarios for the experiments.
• Figure 5: Experiment II Result