Hierarchical Modeling And Verification Of Zone Controller Based On TCSP

The urban rail transit is an important way to solve the traffic jam of big city and makes it convenient for people to travel around. CBTC (Communication Based Train Control) is a system which can ensure the safety and efficient operation of the rail transit. The zone controller (ZC) is the core subsystem of CBTC, which has so many safety functions like train management and calculation of Movement Authority. Simulation and testing methods need large operations and are difficult to complete all aspects for safety verification of ZC subsystem. Given the concurrent distributed complex nature of ZC, a single formal method is difficult to describe. This paper proposes a hierarchical modeling and verification method based on TCSP (Timed Communicating Sequential Process) to do the security research of ZC subsystem.ZC subsystem is divided into system layer and functional layer in this paper. The data of system are regarded as associations between two layers. The real-time character of model is described by the modeling method which joined time mechanism. The system interactive layer is visually described with UML-RT sequence diagram. The semi-formal language UML-RT is transformed into formal language TCSP by using LTS (Labelled Transition System). The hierarchical model of ZC subsystem based on TCSP whose levels are clear and factors are definite is established with TCSP model of internal functional layer. We achieve the model with existing software PAT (Process Analysis Toolkit) which is used for Communicating Sequential Processes and verify the demands of technical specifications related on data based on the LTL assertion.This paper analyzes the cases of task start and normal travel. The train-land interactive system gets MA point according to the system inputs and control rules each cycle and gets the next MA in the same way if there are no faults and emergencies. The system does not meet safety criteria if any retracement occurs. The MA hoppng faults can be found by the fault trace and then we can solve them. So the ZC subsystem can meet the needs of requirements specification and make sure that the system operates normally. And then we can avoid possible defects and errors to a great extent which is meaningful to improve the security of ZC subsystem.