Modeling And Verification Of Level Transition Scene In CTSS-3 Level Train Control System Based On UML And UPPAAL

China Train Control System(CTCS) is the key technology and equipment to guarantee the safe operation of the railway, and CTCS-3 train control system has combined GSM-R with track circuit for the first time. It is compatible with the CTCS-2 train control system as a backup system, needs level transition when CTCS-3 system has malfunction or train enters CTCS-2 section. The success of transition is directly related to train operation safety and traffic efficiency. Therefore, the study of level transition scenario is necessary. CTCS-3 of the train control system specification is the basis of the research and development, modeling and validation can be effective to find the system defects.It is very important thing to ensure the consistency of system and the model on system modeling and verification process. Unified Modeling Language(UML) has a broad application in development researchers for its simple graphics expression and diversification, systems can be expressed meticulously and comprehensively by UML. But UML is relatively inferior in models' validation because it doesn't have the strict mathematical definition. Formal methods can solve this problem effectively, but the fact that its logical expression is relatively complex will bring difficult to ensure the consistency of models and system. The method of combining pattern of UML and timed automata which is the theory to solve the problem of real-time performance has been used in this thesis. UML is used to describe the system firstiy, and then transformation rules which switch UML model into a timed automata model is detailed, finally the model is verified by validation tool UPPAAL to achieve the verification purposes of CTCS-3 level transition scenario.Firstly, the specification of CTCS-3 level transition scenarios is summarized to extract the performance requirements of the system in this thesis. Secondly, the message sequence chart(MSC), UML sequence diagrams and UML state diagram model of two transition ways(C2 level to C3 level transition and C3 level to C2 level transition) are established to achieve consistency of the model and system. This thesis established two kinds of transformation rules based on the commonality of UML sequence diagrams and UPPAAL model.The first rule is from the message sequence chart into UML sequence diagrams, the second rule switched into UPPAAL model through the way of combining UML sequence diagram and UML state diagram. UPPAAL model diagrams under two level transition scenario are concluded according to the transformation rules. Finally, through using validation tool UPPAAL to verify and test the resulting model, the results show that the method to establish the UPPAAL model according to the thesis can satisfy the performance requirements of the system.In this thesis, transformation rules from UML to UPPAAL is drew up in order to achieve the consistency of system and model. The switch process of converting the level transition system to the formalized model which has strict mathematical semantic provides a reference for other complex systems' modeling and validation.