Formal Modeling And Verification Of Cooperative Vehicle Infrastructure System Based On Signal-Controlled Intersection

As a new-generation solution to the urban traffic congestion problem,Cooperative Vehicle Infrastructure System integrates the use of big data,the Internet of Things,and communication technology to ensure the safe and orderly passage of vehicles and pedestrians through each traffic node on the roadway.It also ensures the safe and efficient operation of the transportation system at all times.At present,the cooperative vehicle infrastructure technology has been developed and the pilot applied,and it is in the transition stage of mixed traffic between manually driven vehicles and Intelligent Connected Vehicle.When there is a mixed traffic condition between Intelligent Connected Vehicle and manually driven vehicles at signal-controlled intersections,traditional manually driven vehicles cannot interact with roadside devices and other vehicles with real-time information,and their uncertain behavioral characteristics become a disturbing factor for the safe operation of Cooperative Vehicle Infrastructure System.It is difficult for existing methods to effectively cope with such a mixed traffic state,which brings great challenges to the safety decision control of the intersection Cooperative Vehicle Infrastructure System and intensifies the risk of vehicle collision,rear-end,and other accidents.The formal method is used to construct,statute,and validate the system model employing mathematical logic derivation,which can reduce the dependence on data while carrying out the safety assessment of the scenario system decision.Because of the above problems,this paper proposes a formal theory-based safety assurance method for the Cooperative Vehicle Infrastructure System,based on the study of the intersection Cooperative Vehicle Infrastructure System mixed vehicle control decision mechanism,proposes a formal mapping and verification method for the intersection Cooperative Vehicle Infrastructure System safety and reliability verification,and provides a certain reference basis for solving some technical difficulties of Cooperative Vehicle Infrastructure System at signal-controlled intersections.(1)Analysis of mixed vehicle induction mechanism of signal-controlled intersection Cooperative Vehicle Infrastructure System.Firstly,a quantifiable structured scene of the inlet lane of the signal-controlled intersection is constructed,and the definitions of static and dynamic scene features are given.Then this paper considers the remaining time of the signal and the influence of the manual driver driving style to propose the mechanism of inducing hybrid vehicles by the signal-controlled intersection Cooperative Vehicle Infrastructure System based on the driving decision characteristics of hybrid vehicle and analyze the logic and mathematical constraints of the hybrid vehicle control conditions in the system(2)Modeling the system data interaction process based on the hybrid vehicle guidance mechanism.Firstly,the data interaction process model of the signal-controlled intersection Cooperative Vehicle Infrastructure System based on the hybrid vehicle guidance mechanism is proposed through the domestic specification standards related to the communication and control of Intelligent Connected Vehicle and the hybrid vehicle guidance mechanism,and the system modeling is carried out in a unified modeling language,including the description of system objects,functional state parameters,information migration timing,and functional state changes.(3)Proposed formal analysis and verification method for signal-controlled intersection Cooperative Vehicle Infrastructure System based on temporal automata theory.Firstly,based on the theory of temporal automata,the formal modeling method of the signal-controlled intersection Cooperative Vehicle Infrastructure System is proposed,including the definition of the temporal automata model of the signal-controlled intersection Cooperative Vehicle Infrastructure System based on the unified modeling language,and the action and state migration representation methods.On this basis,the time automaton model transformation rules and the satisfiability verification rules of system safety attributes are given,and the process of system information interaction under the safety induction and safe passage of mixed vehicles according to the signal-controlled intersection Cooperative Vehicle Infrastructure System is analyzed with practical cases to verify the effectiveness of the method.