Safety Analysis And Verification Of Next Generation Train Control System Based On Multi-resolution STAMP Model

The train control system based on train-to-train communication is a typical representative of the next generation of train control system.In the system,train-to-train communication technology is used,moving block technology is adopted for train operation,satellite positioning is used to replace track circuit to realize independent positioning and train integrity checking,and the on-board equipment is responsible for calculating moving authority and autonomous route arrangement.As the train control system is now in the stage of theoretical study and scheme design,it's necessary to carry out safety analysis and formal verification on specific scenarios of the system,to identify the unsafe behaviors and their causes and formulate safety design requirements based on them,so as to avoid the occurrence of dangerous events at the early stage of system design.In this thesis,the multi-resolution STAMP models of train control system based on train-to-train communication are constructed,and the improved STPA safety analysis method is used to analyze the safety of the system under specific scenarios,and many causes of dangerous accidents are obtained;the safety design requirements are defined and validated according to the causes.The main work accomplished in the thesis is as follows:(1)A safety analysis method for train control system based on train-to-train communication was proposed.Firstly,according to the structure and characteristics of the system,the control and feedback process of the train control system examined at different levels for the purpose of improving the traditional STAMP model,and the multi-resolution STAMP models of train control system were constructed to solve the problem that a single STAMP model can not fully describe the complex scenario of train control system,which leads to insufficient safety analysis.Then,since the traditional STPA method cannot distinguish whether the hazard cause is the root cause of the accident,BR(Behavior Relation)was defined in this method to describe the original and non-original causes of unsafe behaviors between various components of the current STAMP model.On this basis,the iterative safety analysis of STAMP models at all levels was carried out along the resolution level and the behavior correlation path until the original causes of all the dangerous events were obtained.Finally,the safety design requirements were proposed based on the original causes.(2)A typical operation scenario was selected to analyze the safety of train control system based on train-to-train communication.Taking the scenario of train following operation from the train depot to the section as an example,which mainly includes the processes of train autonomous positioning,front train identification,train-to-train communication,train autonomous calculation movement authority,etc,and with consideration of the internal structure of the On-Board Equipment(OBE)subsystem,the Dynamic Capacity Decision(DCD)subsystem and Resource Management Unit(RMU)subsystem as well as the information interaction process with external equipment under this scenario,the resolution level was defined and the corresponding UML static and dynamic models were constructed.Through the UML to multi-resolution STAMP model transformation rules proposed in this thesis,the corresponding multi-resolution STAMP models were constructed.On this basis,according to the resolution level,the original causes of all the system hazards were analyzed layer by layer from low resolution to high resolution,and the SDRs under the scenario to be analyzed were proposed according to the causes.(3)The verification for whether train control system based on train-to-train communication can meet the safety design requirements was conducted.The safety design requirements were transformed into BNF statements that can be verified by UPPAAL,and they were divided into three categories: functionality,timing and safety.Under the scenario to be analyzed,the time automata models were established for on-board equipment and its interaction equipment at low resolution level,and the automata network was integrated to verify the BNF statements.The verification results showed that train control system based on train-to-train communication can meet the safety design requirements obtained from the analysis of low-resolution STAMP models on-board equipment subsystem.There are 58 figures,39 tables and 71 references in this thesis.