Parametric Spatio-temporal Modeling And Verifying For TACS Systems Based Train-to-Train Communication

Train Autonomous Circumambulation System(TACS)based on train-to-train communication has become the latest train intelligent control system.This kind of control system can detect the position changes between trains in real time,so as to realize the management and autonomous control of the train workshop.Compared with the trainto-ground communication technology in the traditional Communication-based Train Control(CBTC)system,the TACS system has more streamlined trackside equipment,which effectively shortens the communication time of the train control system and reduces The travel distance of trains improves the operation efficiency of trains,and at the same time reduces the operation and maintenance costs considerably,bringing a great breakthrough for the development of urban rail transit.TACS system is a typical safety-critical system,and the safety of train operation is very critical,so how to guarantee and verify the system safety is very important.Compared with the traditional train-to-ground communication mode,the TACS system based on train-to-train communication has two outstanding characteristics: uncertainty and spatio-temporal characteristics.More frequent train communication makes the system operation environment more complex and changeable,and the uncertain risk from the environment also increases.Therefore,the safety risk research of the train control system is very important.However,the current safety risk research is more focused on vehicle traffic risk prediction.Risk prediction in the direction of rail transit is very rare and relies on expert knowledge and probability analysis,which cannot achieve the purpose of real-time risk prediction.At the same time,the TACS system is convenient and efficient.The train communication mode shortens the travel distance between trains and reduces the response time of system communication,which makes the temporal and spatial behavior of trains more intensive.However,current research on time and space is more focused on time and space logic.As the time and space behavior of the system changes,time and space logic cannot cope with real-time dynamic changes between trains,and thus cannot effectively guarantee the safe operation of the system.In order to solve the appeal problem,from the perspective of formal methods,this paper conducts formal modeling and verifying for the two important characteristics of TACS system uncertainty and spatio-temporal characteristics,quantitatively analyzes its system properties,and achieves the purpose of verifying its safety.The main contributions are as follows:(1)Aiming at the uncertain operating environment of the TACS system,a safety risk prediction method is proposed.This method takes into account the imbalance of the train operation risk states,and is based on an LSTM recurrent neural network as the model framework,which can realize the real-time safety risk prediction of the system.(2)Aiming at the outstanding runtime uncertainty and spatiotemporal behavior of the TACS system,a new parametric spatio-temporal modeling language StHML(p)is proposed.The modeling language models the TACS system by adding time and space elements and inputting safety risk prediction result parameters,and quantitatively analyzes the safety of the system with the dynamic operation of the train.(3)In order to realize the quantitative analysis of the TACS system,a method based on model transition is proposed.This method includes a model transition algorithm and its corresponding mapping rules,which can convert StHML(p)into a networks of stochastic hybrid automaton.The safety risk prediction results are passed to the model as parameters,and then the statistical model checker UPPAAL-SMC is used to quantitatively analyze the properties of the system.This paper takes the operating scenario of the TACS system as an example to illustrate the specific application of the parametric modeling language StHML(p)and the safety risk prediction model during train operation,and combined with the nature of the system,quantitatively analyze the operational safety of the system under different conditions.