Formal Modeling And Verification Method For CTCS-3 System Using TMSVL

Chinese Train Control System level 3(CTCS-3) is one of the core technologies to guarantee trains running safely and efficiency in high speed of 350 km/h. The CTCS-3 system requirements specification is the guidance of the designing and developing for the system. However, for such a real-time and safety-critical system, the dependence on experience of the specification design inevitably exists potential safety hazard or defects. Moreover, if all the system tests are based on real trains running, then it must cost much time and money. Therefore, there should be a way to guarantee the correctness of the specification. Formal method, which is based on rigorous mathematical definitions and can be used to accurately describe specification, is treated as an important method for the system's modeling and verification. In addition, temporal logic as one of the important formal methods, has been widely used in the modeling and verification of real-time and safety-critical system.Timed Modeling Simulation and Verification Language(TMSVL), which is an executable subset of Timed Projection Temporal Logic(TPTL), is a real-time temporal logic programming language. TMSVL is mainly used for the modeling, simulation and verification of real-time system specification. This paper proposes a method for the modeling and verification of CTCS-3 system specification by using TMSVL. First, TPTL, TMSVL and the programming environment TMSV platform are briefly introduced. Then, some core scenarios in CTCS-3 specification are presented. Based on the description of the scenarios' specification, we use TMSVL to build a simplified CTCS-3 model and use Timed Propositional Projection Temporal Logic(TPPTL) formulas to describe some safety and real-time properties. Finally, the modeling and verification process are under TMSV platform and the results are shown.