Hierarchical Formal Modeling And Verification Train Control System

The Train Control System is an automatic system which is integrated of advanced control technology, advanced communication technology, advanced computer technology and railway signal technology. It plays an important role in assuring safety and improving efficiency in railway. The increasing usage of computer technology has led to the increasing complexity in the train control system with large scale of software and hardware, which has exhibited highly distributed, real-time, safety and hybrid properties. As a complex safety-critical system, any fault in train control system can lead to huge human injury or wealth losing. It is necessary to find a more effective and across-the-aboard modeling and verification methodology to guarantee the correctness of train control system. As is compared to simulation technology and testing technology, formal methods based on rigorous mathematics definition have become an important modeling and verification theory in the field of train control systems due to its accurate and clear description of system architecture and related characteristics.A hierarchical model of train control system including system layer, scenario layer, component layer and function layer is proposed firstly by introducing hierarchical modeling conception, using object-oriented methodology and scenario-based design methodology. Based on the hierarchical model, a hierarchical formal modeling and verification framework which is integrated of HCSP, CHARON and TL is proposed. It is not only suitable for verifying all the characteristics of train control system, but also improves the modeling efficiency due to its hierarchical and reused characteristics.The real-time properties of operation scenario in train control system are deeply researched. Six time constraints stated in terms recursion, delay, wait until, time-out, deadline and time interrupt are proposed. Some transition rules are introduced for transiting the HCSP subset models to TA network models. The real-time properties of operation scenario are described using TCTL, and finally a procedure is given for verification based on the simulation.The hybrid properties of operation scenario in train control system are deeply researched. It is pointed that the traditional formal methods of hybrid system are not well in describing communication behaviors which occur in the interactive process of subsystems. To overcome this problem, we introduce a formal modeling and verification method by extending the HCSP syntax and semantics. We transit the HCSP models to HA models by introducing some transition rules based on some assumptions. The hybrid properties of operation scenarios are described using ACTL, and finally a procedure is given for verification based on the simulation.Finally, two typical cases of operation scenario which are RBC handover scenario and movement authority scenario are chosen according to the general technical programming of CTCS level 3 train control system in railways for passengers. Based on the two hierarchical formal modeling and verification models, the real-time and hybrid properties of CTCS-3 train control system are separated verified. As a result, it avoids the maximum fault and error in the system design. It is considered that the method is powerful for solving the key problems in modeling and verification train control system. It is of great significance for ensuring the safety and reliability in train control system.