Research On Modeling And Formal Verification For Autonomous Driving Scenario

There are abundant spatiotemporal data and dynamic behavior interactions in the autonomous driving scenarios,to make them full of complexity.The security of the system is facing critical challenges.In recent years,folks have tried to use scenario modeling and simulation technology to model and analyze the dynamic behaviors of the autonomous driving scenarios.The scenario modeling language and support tools for autonomous driving are still lacking.There is also a lack of formal verification technology to verify and analyze the model.In response to the above problems,we propose an automotive autonomous driving Scenario Modeling Language(SCML),to abstract dynamic behaviors in the driving scenarios and build the system model.Besides,it is proposed to use UPPAAL-SMC to verify the model based on the Network of Stochastic Hybrid Automata(NSHA).The main work of this paper includes:●We proposed an autonomous Scenario Modeling Language SCML,which can construct the scenario abstract model.By analyzing the primary objects and state transitions in the autonomous driving scenarios,abstracted the behavioral randomness and motion hybridity characteristics of the driving scenario dynamic behaviors,designed the formal syntax of SCML based on the Labelled Transition System,designed the meta-model and graphical modeling of SCML based on model-driven theory,and designed the formal semantics of SCML according to the format of process algebra.●We proposed a model-based transformation method to transform the SCML model into the Network of Stochastic Hybrid Automata(NSHA)model,given the specific model transformation rules based on element conversion and rule conversion,and conversion algorithm.Finally,verification engine UPPAAL-SMC was used to verify the safety property of the SCML model of the driving scenario.●We implemented the prototype of the SCML model building and transformation tool.Based on the meta-model and graphical modeling of the SCML,we designed the modeling module of the tool prototype.And the model conversion algorithm is used to convert the SCML model file into the NSHA model file described by UPPAAL-SMC to complete the model conversion.●To illustrate the effectiveness of the proposed approach,we use two classic scenario cases:car-follow scenario and overtaking lane change scenario.We give the corresponding SCML models and transformed them into NSHA models.Finally,using UPPAAL-SMC,a verification tool,and the statistical model checking algorithm,to verify and analyze them.