Formal Modeling and Verification of Autonomous Driving Scenario

There are a buinkint spatio-temporal data and dynamic stochastic behaviors in the autonomous driving scenario, which makes it full of challenges for the modeling and verification of the scenario. In this paper, we propose a Scenario Niodeling Language (SCML) for autonomous driving. SCML can not only express the stochastic dynamic behaviors of autonomous driving but also abstract the primary objects and slate transitions to model the autonomous driving scenario. Firstly, we propose the syntax and semantics of SCML. Then, we construct a metamodel of SCML and propose mapping rules to transform the SCML model into the Network of Stochastic hybrid Automata (NSHA) model. According to the NSHA model, we use UPPAAL-SMC to verify the autonomous driving scenario. Finally, we use the forward-collision warning system to illustrate that the proposed approach can effectively model and verify the driving scenario.