Modeling and verifying safety-critical scenarios of Autonomous Driving System (ADS) have increasingly attracted attention from academy and industry. The major challenge is lacking the domain-specific modeling language for ADS. To deal with this problem, we design and implement an Autonomous Driving Scenario Modeling Language (ADSML) based on the domain knowledge. The metamodel of ADSML describes the modeling elements and their relationships, which is used to capture the specific features of scenario. The concrete syntax of ADSML makes it easy to specify complex relationships among scenario elements, more important, we propose the contract module of ADSML to model the dynamic aspects of scenario. We use the semantics of Stochastic Hybrid Automata (SHA) to specify the dynamic behaviors in scenarios, which is seamlessly integrated with the model checker UPPAAL-SMC. With the help of the automatic model transformation, the ADSML models can be verified with UPPAAL-SMC to analyze the behaviors in scenarios. To demonstrate the feasibility, the scenario of lane change overtaking is modeled and some safety-critical properties are analyzed. The novelty of our approach is that it integrates the advantages of visual modeling and formal modeling. It helps the designers to model and verify the scenario models of autonomous driving systems.

RoboSim is a tool-independent notation for modeling software simulations of robots, and it can be verified by a variety of techniques and tools, including model checking and theorem proving. RoboSim has a formal tock-CSP (Communicating Sequential Processes) semantics, and so refinement checkers, such as FDR, can be used for verification of models. In this paper, we explore the use of UPPAAL, as a well-established tool for verification of time-dependent properties. We propose a model-transformation strategy to translate RoboSim models into NTA (Network of Timed Automata) based on some patterns and mapping rules. We implement our strategy as a plug-in for the RoboSim modeling and verification tool. Using examples, we compare the verification results of UPPAAL and FDR for a series of safety, reachability, and liveness properties. Moreover, we use a robotic platform model of swarm robots in an uncertain environment, to illustrate how our approach can be extended to the verification of stochastic and hybrid systems using UPPAAL SMC. Such an extension cannot be easily conceived for The original tock-CSP semantics of RoboSim.