| Autonomous driving technology can effectively solve traffic safety problems,road congestion,energy consumption,and other problems faced by society to provide a more comfortable traffic environment.Early autonomous driving technology mainly studied driving tasks in specific scenarios,while in the current urban traffic,the automated driving system needs to meet the functions above L3.The decision-making safety assessment of autonomous vehicles in various traffic environments is a current research hotspot and a continuing concern.The difficulty lies in the classification of different traffic scenarios,calculating a large amount of temporary and spatial data,malicious attacks by attackers,and the environmental uncertainty and complexity caused by various artificial driving and autonomous driving mixed traffic.This paper uses formal methods to study and analyze the safety of autonomous driving.The formal method is a rigorous method to support derivation and proof of mathematical logic.Through the modeling,specification,reasoning,and verification of the system model,the dependence of the model on subjective assumptions and non-specific terms can be reduced.Therefore,it is of great significance to apply this method to evaluate the decision-making safety of autonomous vehicles.At the same time,the scenario-based method can significantly reduce the scope of testing,and the effective combination of the two can effectively improve the efficiency of security verification.As the complexity of the driving environment rises sharply,redundant spatio-temporal information has also increased intensively,leading to an explosion of state space.Therefore,the construction of an adequate traffic scene model is the basis for safety assessment,and it also determines the model’s ability to express actual scenes.Second,the decision model directly determines the feasibility and efficiency of the designed model in the face of unpredictable factors.Therefore,corresponding to the characteristics of autonomous vehicles,this paper combines formal methods and proposes a new safety assessment scheme based on existing research,including: 1)this paper proposes an extensible modeling framework for abstract scene features.Extracting abstract scene features through a stable lane adjacency relationship can effectively avoid the phenomenon that the existing research defines the road section adjacency relationship that causes the retrograde path to be regarded as a good road,2)this paper proposes a traffic semantic expression model based on static scene information and a dynamic driving environment.According to the idea of divide and conquer,combined with the continuous dynamic aggregation of vehicles to generate basic semantic scenes,the process of vehicle execution of the entire driving task can be transformed into the combination and connection of semantic scenes to realize the portrayal of large-scale complex scenes.Compared with the existing research methods based on the geometric features of the scene to construct the basic scene structure,the model proposed in this paper can better express the correlation between the scene and the decision,3)Based on the prior probability in the knowledge base,this article shows the random behavior of interfering vehicles and proposes a game estimation model based on semantic scenarios.By transforming the properties that the system needs to meet into the benefits of autonomous vehicles,the decision-making results are more balanced.At the same time,correcting the predicted probability distribution of random behavior according to the instantaneous change of the kinematic data state of the interfering vehicle to meet the actual driving intention of the interfering vehicle can make the optimal response performed by the autonomous vehicle safe enough,4)This article constructs the formal verification process of mathematical credibility calculation by mapping the system model to the automatic model validation tool UPPAAL SMC and applies it to specific case analysis.This article applies the above system model to the spoofing attack case analyzed against the CAM protocol and demonstrates the practical application of the scene model in the field of network security.The experimental results show that the scenario-based formal modeling method in this paper has particular general applicability,and the system model has practicality in the issue of accountability for accidents. |