Generating synthetic driving scenarios in virtual environments is being actively studied for autonomous driving systems, whose safety is challenging to verify in physical environments. While several works proposed a way to describe such driving scenarios called Operational Design Domain (ODD), their syntax still lacks formal semantics, which makes it difficult to design trustworthy compilers -a software that converts an abstract scenario expressed in ODDs into a concrete scenario executable in a virtual environment. We propose a systematic way to formalize the lane-level driving scenarios described using a subset of ASAM OpenSCENARIO syntax. In particular, our formalization exploits the concept of separating concerns in which an abstract scenario is described without exposing the low-level behavioral details of autonomous driving; the details can then be auto-filled during the concrete scenario generation via different objectives. We define the decision variables that need to be determined when generating concrete scenarios; then, we propose a set of constraint categories that restrict the valuation space of the variables according to the syntactic structure of an abstract scenario. We implemented two compiler designs as exemplar based on two solvers: one with SMT (Satisfiability Modulo Theories) and another MILP (Mixed-Integer Linear Programming) solvers, and show the qualitative and quantitative analysis of concrete scenarios auto-generated from an abstract one.
