Formal Modelling And Verification For Safety Analysis Of Automated Driving

With the rapid development of information science and technology,new complex systems such as Cyber-Physical System(CPS)are gradually integrated into human social life.As a classic application scenario of CPS,automatic driving is based on the per-ception of the driving environment and makes corresponding driving decisions through calculation.It has the characteristics of autonomy and safety.However,the complex and changeable urban scenarios,a large amount of real-time spatio-temporal data,and inherent uncertainties in the external driving environment all bring challenges to ensure the safety of automated driving.This thesis adopts the formal method to study and analyze the safety of automated driving.The formal method employs mathematical(logical)proof to model,specify,analyse,reason and verify the computer system.Due to its rigour,this method has been widely used in system safety research.However,due to the above characteristics of automated driving,there are still many challenges in the formal method.For example,most spatio-temporal constraints are modelled based on differential equations now,which is not conducive to the abstract analysis of spatio-temporal constraints.Furthermore,for the problem of state space explosion,it is necessary to propose an abstract formal modelling method and mod-elling the uncertainty.Based on these,it is also necessary to study how to transform the safety analysis problem in verification into a decision problem based on the formal model,and to verify whether the safety properties of the system are met.In this thesis,based on the characteristics of automated driving system,utilizing the formal method,with the safety assessment of automated driving as the research objective,the formal modelling and verification method of the automated driving system based on the spatio-temporal abstract model is studied.The main research contents and contributions of this thesis are as follows:· Bounded Multi-dimensional Modal Logic(BMML)is proposed based on the per-spective of the autonomous vehicle.This logic can specify the constraints based on relative time and space and support the reasoning of spatio-temporal constraints.· The scenario definition and scenario composition methods are proposed.The fun-damental scene structures are defined according to the scenario definition and cor-responding spatio-temporal constraints to be satisfied.Based on the fundamental scene structure,scenario transformation can be realized according to the connectiv-ity,and various complex scenarios can be combined from the fundamental scene structures according to the composability,which lays the foundation for the model verification framework based on the scenario.· The abstract model of an automated driving system based on the scenario is con-structed.Based on environment perception,the abstract model can describe traffic data from real-time observation and estimation and use a probability model to ex-press the uncertain driving decisions of vehicles other than the autonomous vehicle explicitly.· Automated verification of safety properties is realized.Based on the verification framework of the abstract model,the abstract model is transformed into Stochas-tic Hybrid Automaton(SHA)by establishing the mapping relationship of features.The verification tool UPPAAL SMC is used to realize the automated verification of qualitative and quantitative safety properties.This thesis takes multi-lane round-about as an example to demonstrate the practicability and universality of the formal modelling and verification method based on the scenario.