STPA Based Safety Analysis Of Rdc In CTCS-1 Train Control System

The Chinese Train Control System level 1(CTCS-1)is suitable for existing railway lines and the newly-built ones with speed below 200km/h,which uses the distance to go mode to supervise train operation.Since it is still under development,it is necessary to carry out safety analysis and risk assessment to find out whether there are some unsafe factors in the specific application scenarios.As a key trackside subsystem,RDC is a real-time multitasking system,whose core functions include receiving information from Centralized Traffic Control(CTC),Computer based Interlocking(CI),and Temporary Speed Restriction Server(TSRS),and receiving train position report from the On-Board Equipment(OBE)via GSM-R.Based on these information RDC generates Movement Data(MD)and transmits the MD and the Temporary Speed Restriction(TSR)to OBE.In this thesis,the combination of the Systems Theoretic Process Analysis(STPA)and the UPPAAL verification method is adopted to conduct safety analysis,modelling and verification on the core functions of RDC system.Among various safety analysis methods,STPA can identify risks in a systematic,modular and accurate way.The main works of this thesis is as follows.(1)Firstly,by taking the scenarios of MD generation and TSR sending as example,the safety analysis of RDC system was conducted by following the STPA process.The identification of hazards and corresponding accidents were carried out.The Internal Block Diagram(IBD)in SysML was used to describe the hierarchical control structure;the process model of RDC was established,and the related systemic Unsafe Control Action(UCA)and Control Flaws(CF)that lead to hazards were identified.Finally,the related constraints and Safety Design Requirements(SDRs)were generated.It should be noted that these SDRs are the source of verification sentences in UPPAAL.(2)Secondly,based on the main operation scenarios,the related SysML diagrams for RDC were built and then were converted into Timed Automata models.According to operation scenarios,the RDC information control processes were categorized into equipment startup,train registration,train movement and train deregistration,and the SysML sequence diagrams were used to describe these processes.Besides,the SysML sequence diagram,activity diagram and state machine diagram were used to describe the TSR scenario.In addition,the ATL(Atlas Transformation Language)method was used to transform the models.The transformation process includes establishing SysML meta-model,and timed automata meta-model,and establishing the clear transformation rules from SysML sequence diagram,activity diagram and state machine diagrams to Timed Automata model.Based on the ATL method,the SysML models were converted into Timed Automata models.(3)Finally,the combination of safety analysis based on STPA and UPPAAL verification are completed to verify whether RDC can satisfy the SDRs and corresponding functional requirements.The SDRs obtained in STPA analysis were formalized as verification statements of BNF(Backus Normal Form)in UPPAAL.Then,these BNFs were classified into three types including logical functions,time sequence functions and safety properties.Besides,the transformed Timed Automata models were simulated and verified via the UPPAAL model checker.The analysis results show that the combination of the STPA with the UPPAAL can perform effectively to analyze the safety of RDC.