Formal Modeling And Verification Of Level Transition Scene In CTCS-3 Train Control System

With the rapid development of China’s economy,the development of railway has entered a golden period.At present,our country’s lines mostly use Chinese Train Control System(CTCS-3)train control system,and the level transition scenario,as one of the main scenes of the CTCS-3 train control system,plays a very important role in ensuring normal train transition and failure transformation.The CTCS-3 train control system requirement specification serves as a prerequisite for system development and describes the related functional requirements and performance requirements that are necessary for the hierarchical transition scenario.The success or failure of the system’s level transition directly affects the train’s operational safety and driving efficiency.The length of the level transition time and the train’s operating speed are of great significance to ensure the safety of the system.Therefore,taking the level transition scenario as the research object,the formal modeling method as the starting point,the requirement specification of the train control system as the criterion,It is necessary to formally model and verify its level transition scenario.The key to modeling and verifying of the system is to ensure the consistency of the system and the model.Unified Modeling Language(UML)has a broad application in development researchers for its simple graphics expression and diversification,system can be impressed meticulously by UML.But its lack of model validation.Formal methods can solve this problem effectively,the fact that its logical expression is relatively complex will bring difficult to ensure the consistency of medols and system.The method of combining pattern of UML and CPN theory which is the method to formal modeling of level transition scenario.Firstly,according to the summary of the system requirements specification,two levels of transition scenario under normal conditions are described.Secondly,the UML models of CTCS-2 to CTCS-3 level transition and CTCS-3 to CTCS-2 transition under the two transition methods are established respectively to realize the description of the message interaction process and the static transition process of the transition scenario.According to the requirements of the system to analyze the performance and functional requirements of the hierarchical transition scenario,formulate the conversion rules from the UML model to the colored Petri net model,and convert the established hierarchical transition scenario UML model into a colored Petri net model.Using validation tool CPN Tools to verify and test the resulting model,it verifies the correctness of the model structure and logic,so as to achieve the consistency of system and model.Finally,through modeling the simulation run,the extracted operation data is simulated by MATLAB.The relationship between train running speed,transition time and transition success rate is obtained.The factors affecting the stability of the level transition are discussed.The results show that the method to establish the colored petri net model according to the thesis can satisfy the performance requirements of the system and provides a reference method for the formal modeling and verification of other complex systems.