Specification and Validation of Autonomous Driving Systems: A Multilevel Semantic Framework

TL;DR

This paper introduces a multilevel semantic framework for specifying and validating autonomous driving systems, focusing on formal map modeling, logical specification, and validation techniques to address complex validation challenges.

Contribution

It presents a novel multilevel semantic framework with formal map definitions and configuration logics for improved specification and validation of ADS.

Findings

Maps modeled as directed metric graphs with geometric consistency

Introduction of Configuration Logics with coalescing operator for map configurations

Framework supports run-time verification and scenario specification

Abstract

Autonomous Driving Systems (ADS) are critical dynamic reconfigurable agent systems whose specification and validation raises extremely challenging problems. The paper presents a multilevel semantic framework for the specification of ADS and discusses associated validation problems. The framework relies on a formal definition of maps modeling the physical environment in which vehicles evolve. Maps are directed metric graphs whose nodes represent positions and edges represent segments of roads. We study basic properties of maps including their geometric consistency. Furthermore, we study position refinement and segment abstraction relations allowing multilevel representation from purely topological to detailed geometric. We progressively define first order logics for modeling families of maps and distributions of vehicles over maps. These are Configuration Logics, which in addition to the usual logical connectives are equipped with a coalescing operator to build configurations of models. We study their semantics and basic properties. We illustrate their use for the specification of traffic rules and scenarios characterizing sequences of scenes. We study various aspects of the validation problem including run-time verification and satisfiability of specifications. Finally, we show links of our framework with practical validation needs for ADS and advocate its adequacy for addressing the many facets of this challenge.