A quantitative safety verification approach for the decision-making process of autonomous driving

Autonomous driving is a safety critical system whose performance mainly depends on the recognition of the environment through a large amount of spatio-temporal data and driving policy based on the complex traffic conditions. Thus, it is important and necessary to build the abstract model of environment data and set the safety assessment method for autonomous driving policy. To address the problem, we propose a quantitative safety verification approach for the abstract decision-making model of autonomous driving. We extract the essential spatio-temporal features from both observation and estimation, and preserve them in the abstract model of decision-making. In the estimation, we adopt the explicit description of the uncertain driving decisions of vehicles by means of probability distributions. Based on these time-dependent spatial features, specification, reasoning, and verification of safety property are enabled. To evaluate the safety of the driving policy, we propose an operational verification approach based on Stochastic Hybrid Automata (SHA). Given the environmental information and the corresponding driving decisions according to the planned route on the basis of certain traffic laws, the single-lane roundabout scenario is introduced to illustrate how to verify quantitative safety property in our verification approach by using UPPAAL SMC which can validate the stochastic real-time model.