Research On Safety Analysis Method For RBC Handover Based On NuSMV And STPA

Chinese Train Control System Level 3(CTCS-3),as the core equipment of Chinese high-speed railway,is responsible for ensuring the safety of high-speed trains,and also is the "nerve center" of high-speed railways.The safety of CTCS-3 system plays a key role in the safety operation of high-speed railway.The radio block center(RBC)handover scenario is an important operation scenario of the CTCS-3 system.It is significant for ensuring the safety of high-speed railway to study on an effective and scientific safety analysis method according to the characteristics of this scenario.However,both the functions and the component interactions of the CTCS-3 system are complex.This will bring challenges to the application of traditional safety analysis methods in analyzing this system.As a new technology based on System-Theoretic Accident Model and Process(STAMP),System-Theoretic Process Analysis(STPA)treats abnormal interactions among components as the main causes of system hazards,which meets the requirements of safety analysis methods to the CTCS-3 system.However,there is no unified method to describe the model at present,and the use of natural language to build the model will be easily influenced by the human expression ability.In addition,the STPA analysis is mainly done manually,which leads to that the credibility of the analysis results will be affected by the analysts' experience.To overcome the shortcomings of the current modeling and analysis method,the scalability and other advantages of Unified Modeling Language(UML)are untilized to improve the modeling method for the hierarchical control structure in STPA,and the characteristic that NuSMV can give counterexamples automatically is untilized to assist in implementing the STPA safety analysis process.The main contents include:(1)Based on the understanding and reading of a large number of domestic and foreign literatures,this thesis briefly introduces the current research of safety analysis methods,and moreover compares and analyzes the advantages and disadvantages of different safety analysis methods.This makes clear the research prospects of existing safety analysis methods in train control fields.(2)An UML profile for STAMP model is designed,in which the UML class diagram and control feedback messages are extended,i.e.,the STPA method is extended to depict the hierarchical control structure model of the system to be analyzed.(3)The semi-formal UML model is transformed into formalized NuSMV model,and Functional Failure Description Symbol(FFDS)and Fault Pattern(FP)are constructed to describe the possible functional module failure.The normal behavioral model of the system is integrated with the fault model to form a NuSMV model that includes the fault set.Then the method of model checking is utilized to creat the control flaws analysis method.(4)According to the characteristics of RBC handover,the research case is described from static structure and dynamic behavior,and the hierarchical control structure model in case is created by UML extended profile.The UML class diagram is used to describe the hierarchical control structure,the state diagram is used to describe the control algorithm,and the OCL language is used to describe the process model.(5)The extended STPA method is untilized to analyze the control flaws of RBC handover.Firstly,a system-level hazard is chosen.Then,the unsafe control actions are identified.And then the unsafe control actions of the system are taken as properties,which are analyzed by the model checking tool NuSMV.Finally,the control flaws of the system are identified from the established fault set.