Modeling And Analysis Of RBC Handover Based On UML And Colored Petri Nets

Radio Block Center (RBC) is one of the core ground subsystems of the Chinese Train Control System at Level3(CTCS-3), and is one of the key equipments to ensure safe operation of trains. RBC is a complex and safety-critical system. In order to ensure the correctness of the RBC system, a comprehensive and effective method of modeling and verification is needed. With RBC handover as its object, the present thesis carries out the study of modeling.By giving a description of the RBC’s working principle in the CTCS-3, the security and functional requirements of RBC are cleared. The complementarity of Unified Modeling Language (UML) and Colored Petri Nets (CPN) is found from the comparative analysis of their advantages and disadvantages. For this reason, these two modeling methods can be combined to apply. The modeling scheme of RBC is designed based on the integrated modeling method. Moreover, the basic rules for converting UML to CPN are studied.In order to verify the effectiveness of the integrated modeling method, the function requirements and strategies of the RBC handover are analysed in depth, and the thesis has put more efforts into application study of the method in the double-radio handover. Firstly, the handover flow with double-radio is designed. Secondly, the UML use case diagrams, sequence diagrams and state diagrams are used for describing characteristics of the handover. And according to the rules for converting UML to CPN, CPN model is built. With hierarchi-cal modeling idea, finally the whole hierarchical CPN model of RBC handover is constituted.The CPN Tools is used for verifying the functionality of the established hierarchical model. The appropriate state space report and o-graph are generated by the analysis of state space tool-box. Boundedness properties, home properties, liveness properties and fairness properties as dynamic properties of the model are explained in the report. The logical correctness of the model is reflected in the o-graph, and the state queries order is utilized so as to examine the consistency of the model’s features and the design original intention. Results show that functional properties of RBC handover can be reflected in the established model.The whole hierarchical model has complete functions after being examined, some time factors are put into the model, and the CPN model can be turned into the timed CPN model. The monitors in the CPN Tools are used to collect simulation data of the model. Through simulation of the timed CPN model runs many times, the analysis of the time performance under the different quality of communication can be obtained. The results are helpful to perfection of the RBC system design.