TSC2CARLA: An abstract scenario-based verification toolchain for automated driving systems

Transitioning automated driving systems to complex operational domains disproportionally increases demands on verification activities. In the worst case, the operational domain can not be covered by a manageable set of logical scenarios. An anticipated solution is to use abstract scenarios, which increase coverage while still enabling formal methods. However, established verification approaches must be adapted for abstract scenarios. In this work, we consider the generation of simulatable test suites from abstract scenarios. For this, we use Traffic Sequence Charts (TSCs), a visual yet formal scenario description language based on first order logic. We propose an SMT-based process for generating concrete test cases that can be simulated in e.g. CARLA. This theoretical framework is compiled into an architecture and a prototypical implementation called TSC2CARLA. An evaluation on a set of non-trivial examples yields initial evidence for the feasibility of our approach.