Monitoring Safety Properties Of Train Control System Based On Run-Time Verification

The train control system is one of the vital component of railway transportation system and which ensures the safety during the train is running. Testing and formal verification is the chief ways to guarantee its safety. Traditional test methods can hardly test all the possible environment and routes because of their incompleteness, so it cannot insure that the systems been tested are without safety drawback. Model checking is a kind of complete test method, but it would encounter the contradiction between the ability of description and verification, especially when the states exploded, this method would not be feasible for the complex system. Runtime verification is a kind of light weighted verification technique and it verifies the system while the target system is working. It can timely monitor if the execution route of the system satisfied the safety properties. Gradually being focused on in many area, runtime verification is getting applied into several high safety industry as a effective complement to the traditional verification techniques.This article starts with the some serious problem such as bad branching in the train control system and Radio Block Center switching and then studies the corresponding runtime verification techniques, including:(1) This article analyzed the scene and reason of bad branching in the subsystem of railway circuit and then concluded a group of key properties of monitoring on bad branching in order to ensure the train's safety. This article presented a method to depict and generate monitors in LTL. As the bad branching problem needs multiple monitors work contemporarily, this article presented a scheduling strategy of multiple monitors aiming at bad branching problem, which is expected to improve efficiency.(2) In order to implement the auxiliary description and automatic generation of monitoring properties, this article extended the Java MOP monitoring tools, redesigned MOP file format, expanded the definition language of events and conditions and then implemented corresponding monitor generator tools aiming at the main features concerned by the safety monitoring of the train control system, including the description of monitoring events, the non-instrumenting running mechanism of monitors and the C implemented train control system.(3) In order to verify the validity of the above methods and tools, this article conducted experiments on the scene changing process of Radio Block Center subsystem in the train control system. Specifically, this article specifies the safety properties needed to be satisfied by the RBC connection process and generated corresponding monitors in order to discover the danger timely. The experiments results is desirable, thus the feasibility of above methods and the validity of prototype tools has been verified.