The Study On Formal Modeling And Verification Of High-speed Railway Train Control System

With the extensive application of advanced computer, communication and control in high-speed railway train control systems, the efficiency and safety have been greatly improved. Because the integration density of hardware enhances and more software participate in control, many new related system characteristics have appeared, like the distributed structure, hard real-time capability, fast response and so on. So the verification of system characteristics becomes more and more difficult, and a solution which can realize the effective and across-the-board verification of high-speed railway train control system should be proposed, and make the system performance and function more improved. The formal methods based on rigorous mathematical definition have developed rapidly in the field of the train control systems, because they can accurately and clearly describe the related characteristics and structure, and verify these characteristics as well, in recent years, they have become an important way to describe and verify the high-speed railway train control system.The formal methods of modeling, description and verification for train control system are discussed and summarized at the first. The advantages of RAISE (Rigorous Approach to Industrial Software Engineering) formal method being applied in the modeling and verification to train control system is analyzed, and on the basis of these analyses, the Timed RAISE is introduced into the verification field of train control system for the first time.The modeling and formal description method which based on the Domain & Timed RAISE for high-speed railway train control system is studied. Combined with the actual characteristics and complexity of high-speed railway train control system, a Domain Method is proposed and this method can be a breakthrough point of system modeling. The main idea of Domain Method is that the system can be divided into small-scale domain models, in accordance with the results of domain's verification and the relation of combination and decomposition between domains, and then the characteristics verification of whole system can be realized.The relative definitions and theorems about domain tuples, domain combination and domain characteristics are defined in detail, these definitions and theorems are the key components of theory system of Domain Method. In order to give a better illumination to Domain Method, the representative high-speed railway train control system-CTCS-3 (China Train Control System level 3) is divided into domains, and the domain models are built, the domain characteristics are analyzed, the domain characteristics are combined and decomposed and sub-domains are divided in practice, and this practical example mighty supports the theory system of Domain Method.The verification method based on the Domain & Timed RAISE method for high-speed railway train control system is discussed. Three kind common and important domain characteristics of train control system are analyzed in detail:the relative characteristics of scene description, system function and system performance. And accurate mathematical definitions and descriptions of three specific characteristics are given, namely the scene interactive consistency, fundamental safety function and the real-time capability, these definitions and analyses serve as the important base of the verification to system characteristics.The integration of Domain Method and Timed RAISE is achieved, the concrete transformation rules from domain models to TRSL (Timed RAISE Specification Language) are given, and the relevant reasoning rules and specific proving methods in the verification process of TRSL specification are given as well.Some application examples of Domain & Timed RAISE method have been given. The characteristics verification of scene interactive consistency in RBC (Radio Block Center) handover scene, real-time capability in level transition (CTCS-2 to CTCS-3) scene, the safety function during trains pursuit in wayside railway is achieved, and the division of the real domains, the establishment of system models, the formal description and reasoning of Timed RAISE are analyzed and discussed in detail. To merely explain the correctness and validity of Domain & Timed RAISE method, these examples and cases have been simplified and adopt some assumptions. Finally the results are given: on the condition of one train passed the boundary between RBCs, the interactive process between onboard equipment and RBCs will not cause the errors of the scene interactive consistency; in the scene of level transition (CTCS-2 to CTCS-3), even if the uncertainty of GSM-R (GSM for Railway) wireless network is a tremendous challenge to the real-time capability, but this scene still satisfies the real-time requirements; in the case of two trains pursuit, after ascertaining the conditions of head train and the boundary of external environment, CTCS-3 can ensure the safe operation of objected train under the co-action of ground equipments, onboard equipment and GSM-R wireless network.