The Modeling And Verification Method For Hybrid Behavior Of Train Control System

With the development of science and technology, the Train Control System has a great development and progress. In order to ensure the safety of the Train Control System, Train Control System’s System Requirement Specification (SRS) has played a more and more important role in research and development. However, in the initial stages of system development, how to determine the key parameters of the system requirement becomes a new research topic in the context that the system requirement is not complete or right enough to undertake the design and development. However, current studies show that there exist a lot of difficulties for the key parameters analysis and validation work on SRS level for guaranting the critical properties of the train control system. As a result, a reasonable framework should be proposed for system property modeling and system formal verification.The analysis process of the Train Control System Requirement Specification includes two parts. One is setting up the system’s formal model, the other is verifying the system model by verification tools. On the one hand, Unified Modeling Language (UML) is a widely used object-oriented visual unified modeling language, which has been applied in different domains. However, the Train Control System is a typical hybrid system and safety-critical system. Describing hybrid system’s hybrid property is a big challenge for the modeling work of Train Control System’s SRS. On the other hand, formal methods, which are used for improving the safety-critical system’s safety and reliability, are available for the verification of SRS. Among various formal verification tools, researchers can choose different formal verification tool to verify the formal models according to the different requirements for analysis or verification.The focus of this paper is to research on the modeling method for hybrid system 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 useful for system modeling. 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, hybridUML Profile is proposed for Train Control System’SRS.2. For realizing the safety verification of the hybrid system, the Reachability Analysis Algorithm of Bounded Time are provided, which is based on the Bounded Model Checking (BMC) verification method. The all executable path in finite time bound for a specific model can be computed by the aforementioned algorithm, which can solve both the linear and nonlinear hybrid automata for hybrid systems.3. As for case study, the pursuit model of "Moving Block System" was chosen. By the proposed modeling method based on UML Profile, its hybridUML model was set up. Then, the extended UML model of pursuit models are transformed into formal verification model such as HYTECH model, HySAT 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 hybrid behaviour.4. A new verification tool on Topcased platform is proposed. With the good expansibility, the tool integrates the existing UML model tool Papyrus, and verification tools (HYTECH, HySAT and PHAVer) by expanding views on the Topcased platform, 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 extended UML model to formal verification model such as HYTECH model, HySAT model and PHAVer model are given respectively.