Modeling And Verification Of Zone Controller For CBTC System Based On CPN

With the significant development of communication technology,computer technology and control technology,the transmission method of urban rail transit information has been changed from wired transmission to wireless communication.Communication Based Train Control(CBTC)has gradually become my country’s An important part of urban rail transit.The Zone Controller(ZC)generates Movement Authorization(MA)for the vehicle by frequently exchanging information with other subsystems of the CBTC system,and is an indispensable safety control device for the CBTC system.Analyzing the structure and function of the zone controller,and constructing a model that satisfies the safety and real-time characteristics of ZC handover,which is conducive to the safe and efficient operation of trains on the line.Based on the original modeling method,the dissertation adopts the means of combining Unified Modeling Language(UML)and Hierarchical Timed Colored Petri Net(HTCPN)to analyze the relationship between CBTC subsystems in the ZC handover scenario.Modeling and verification of the information exchange process,and based on the obtained model,the security analysis of the ZC handover scenario is carried out.The specific research work is as follows:(1)According to the "Technical Specification for Urban Rail Transit CBTC Signal System Industry-Product Specification" formulated by China Association of Metros,the basic composition and working principle of the CBTC system are analyzed.With the help of flowcharts,the handover process of the zone controller and the generation of movement authorization under the handover scenario are analyzed,and the UML use case model,sequence model,state model and activity model are constructed according to the requirements of the two functions.(2)The constructed activity model nodes are extended into executable intermediate model nodes by using the extension mechanism of UML,and the executable intermediate model is converted into a hierarchical time colored Petri net model by combining XML technology.Then,the converted HTCPN model is verified with the help of the state space report and ASK-CTL formula in CPN Tools,the simulation verification tool of Petri net.The verification results show that the system properties and dynamic properties of the HTCPN model are normal and meet the functional requirements of the ZC handover scenario.(3)The extension mechanism of UML is used to mark and extend the nodes of ZC state transition diagram and train state transition diagram,and the PHAVer model is generated according to the transformation rules.A fault integration algorithm is used to integrate the PHAVer model and the fault model into a fault-containing PHAVer model.The forward reachable set calculation principle and the fault monitor model are used to simulate and calculate the PHAVer model containing faults,and find the fault event cut sets that endanger the system safety,and the safety analysis of the ZC handover scenario is carried out according to the relevant fault combinations.(4)The All Paths Covered Optimization Algorithm(APCO)is used to search the path of the state space reachability graph generated by the HTCPN model,and the search results are converted into a test case frame with the help of XML technology.Referring to "TCMAET04012.1-2018 Interconnection Test Specification for Communication-Based Train Operation Control System of Urban Rail Transit" and the situation of Chongqing Line 10,the fault event was selected as the test case object and tested on the CBTC general test platform.The test results show that the fault test cases obtained through the full path coverage optimization algorithm search meet the requirements of the urban rail test specification and the functional requirements of the ZC handover scenario.Through the results of model simulation and case testing,it can be seen that the model established by the combination of HTCPN and UML can not only ensure mathematical rigor,but also clearly describe the entire process of ZC handover and movement authorization generation.Through the HTCPN model state space The test cases calculated by the reachability graph also meet the requirements of the test specification,which proves the practicability of the integrated modeling method,and provides a reference for the modeling and testing of other functions or scenarios of the CBTC system.