UML Domain Modeling Method For Train Control System And Verification Tools Integration

With the development of science and technology, Train Control System’ functions have developed into a new stage. In order to realize the connection between different equipments produced by different manufactures, and to insure the safety of the Train Control System at the same time, Train Control System’s System Requirement Specification (SRS) has played a more and more important role in research and development. However, current studies show that there exist a lot of difficulties for the analysis and validation work of the critical properties in SRS level. As a result, a reasonable framework should be proposed for property modeling and system verification.On one hand, from the view of modeling method, Unified Modeling Language (UML) is a widely used object—oriented visual unified modeling language, which has been applied in different domains, however, describing hybrid system’s property is beyond UML’s ability, which seems to be a big challenge for the modeling work of Train Control System’s SRS.On the other hand, formal methods, as means of improving the safety-critical system’s security and reliability, are available for the verification of SRS. There exist various formal verification tools. Researchers have the right to decide which formal verification tool is the most suitable one, according to the different systems, different system properties, and different phases of system analysis.The focus of this paper is to research on the modeling method and the integration of formal verification tools for Train Control System’s SRS. The works of this paper are summarized as follows:1. Firstly, UML2.0and its extensibility mechanism UML Profile are helpful to find a modeling method. For the purpose of providing a possible way to describe and analyse the hybrid property of the Train Control System’s SRS in formal methods, a new modeling method is proposed, based on UML Profile for Train Control System’ SRS.2. By researching the analysis framework structure of SRS, the requirements raised in verification phase are emphasized. A new idea of developing a verification support tool on Eclipse platform is proposed. With a good expansibility, the tool integrates the existing requirement management tool (IBM RequisitePro), modeling tool (IBM Rational Software Architect), and verification tools (NuSMV, PHAVer) successfully, and completes the low-level modeling work and formal verification work in the background. What’s more, as a part of verification phase’s work, the transition rules for the transition from the UML model to NuSMV model and to PHAVer model are given respectively.3. As for case study, the "Modes Transit" and "RBC Handover" scenarios are chosen. Following the proposed modeling method based on UML Profile, the scenario UML models are transformed to NuSMV model or PHAVer model respectively, according to the transition rules. And later, verification work is completed using the verification support tool built already. The result shows that the modeling method and the verification software tool seem to be feasible and appropriate for the analysis of Train Control System’s SRS.