Security Modeling And Validation Of Movement Authority In CBTC System

In recent years,Chinese urban rail transit industry has achieved a leapfrog-development.The utilization of operation system,namely the Communication Based Train Control(CBTC)system,has become the mainstream trend of urban rail train control system by virtue of its safety,reliability and efficiency.In urban rail transit,the train is guided safely by movement authority(MA)information,so the security implementation of the function of Movement Authority is crucial.However,due to the complex logic and strong real-time performance of function,any minor errors or design deficiency in the internal modules may lead to fateful consequences.In order to find out the possible ambiguity or inaccessibility in each module more accurately,it is of extremely significance for the safety of urban rail transit to adopt a formal method in modeling the function of movement authority and check the functional requirements of each module in the process of developing the functional system.The research object of this dissertation is the movement authority’s function of CBTC system.This function is described and analyzed in detail by using time automata theory.The model verification tool UPPAAL is used to verify the robustness,real-time,accessibility and security of function.Firstly,the basic structure and working principle of CBTC are analyzed,especially the functional principle of movement authority.From the perspective of different functional modules,the time automata models of train screen module,train manage module,safety location module,ergodic obstacle module and movement authority generation module are established to form the time automata network model of movement authority.Secondly,under different operating scenarios,the process by which movement authority function is implemented according to different logical processes is analyzed.The functions of each module are realized by the interaction of different device information.as a consequence,a hierarchical structure of movement authority in each scene is established.The idea of hierarchical structure is introduced into time automata theory,and the hierarchical model of time automata network for movement authority in each scenario is established,including top layer,scene layer,function layer and equipment layer.Finally,the network model is simulated in the simulator window of UPPAAL,and the message sequence diagrams representing the information interaction between sub-models are obtained.The backus-naur Form(BNF)grammar is used to compile the validation statements of different models in terms of function and security,and the validation is carried out in the validator window to verify the robustness,real-time,accessibility and security of functional model.It provides a theoretical reference for the in-depth study of functions of the CBTC system in the later stage,and the hierarchical time automata theory also effectively solves the complex process and logic in modeling,which can be applied to the development and verification of urban rail transit control system.