Research On Modeling And Verification Based On UPPAAL And Its Application To CTCS-3Train Control System

CTCS-3Train Control System, a real-time wireless transmission system based on GSM-R working for delivering bidirectional messages between RBC and train, is the highest current application level in China. In the course of the localization of Train Control System, researches and verifications of CTCS-3technical specification are crucial for ensuring safety and high efficiency. In real-time systems, a tiny logical error can lead to unpredictable disastrous consequences, so model verification is our best choice. However, the challenge is how to ensure the correctness of real-time model.Guaranteeing the consistency of the model and the system is the first step to achieve the goal of verification. The models we need should not only have the ability of depicting the real-time system precisely, but also prossess extensive application basis among developers. UML meets the above requirements, but it can not do anything about model verification. Formal verification has unparalleled advantages in model simulation and verification, however it is very difficult to translate literal specification directly into models using formal languages. Verification on the premise of unanimousness between model and system can be done if there is a bridge between these two models. Timed automata are used in this paper as the formal modeling tool combining with UPPAAL.The analysis about RBC handoff scene has been done at the head of Chapter2. Also, UML is extended to aim at researching real-time system. Next, sub-models have been made by using extended UML sequence diagram according to several event sets which are devided by three key time points. Then, piece together these sub-models making the integrated sequence diagram of RBC handoff. The purpose that the whole process is modeled by several event sets facilitates the later transformation of timed automata model.Following the related semantics of timed automata and combining with the characteristics of Train Control System, sub-models are integrated into an unabridged model. General rules of transformation are given in this paper.A timed automata network model is made by merging the independent timed automatas acquired. State transition graphs are engendered by emulating the network model using UPPAAL. The formal verifications about deadlock of the model and the system functions can be done by BNF statements extracted from literal specification, so as to achieve the purpose of the research on specification. The combining of UML model and UPPAAL timed automata reaches a high degree of unity in expressing specification semantics and model check. And this provides a reference in the research of CTCS-3Train Control System.