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

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.