Research On Verification Method For Safety Communication Protocol In Train Control System

As wireless communication has the advantages of high transmission speed, bidirectional transmission and so on, the train control systems have been gradually developing from track based train control to communication based train control. The train and trackside must communicate with each other safely, as the train control system is a safety-critical system. However, there are a series of threats in the wireless communication system, such as repetition, deletion, insertion, resequence, corruption, delay, and masquerade, which could not guarantee the safety of data transmission, meeting the requirements of safety communication in train control system. Safety communication protocol is induced in this situation. Safety communication protocol runs in a safety-criticial environment, and in essence it is one communication protocol. Therefore, the verification of this protocol includes not only safety function, but also protocol performance, which brings about challenges to verification of this protocol.Based on the characteristics of safety communication protocol in train control system and the in-depth analysis of the focus and limitation of the existing verifying approaches for communication protocol, this paper has determined that the content of verification for safety communication protocol includes function and performance. This paper integrates model checking and simulation to verify safety communication protocol, making used of model checking and simulation supported by Colored Petri Net (CPN). On the basis of the hierarchy architecture of communication system in the European Train Control System (ETCS) specified in the ETCS protocol specification, the thesis establish the models of safety communication protocol, viz. safety layer, application layer, and channel respectively, making use of the hierarchical function of Colored Petri Nets (CPN). Referenced from the temporal logic of safety communication protocol defined in the protocol specification, the correctness for the logic, as well as the time under ideal condition of the protocol are verified with ASK-CTL, which is a model checking tool based on Computational Tree Logic (CTL) supported by CPN. The results of verification could meet the expected results, preliminary showing that the verification method is reasonable. Furthermore, on the basis of some specific technical indicators in the train control system during the implementation, the timed characteristics of the protocol in a stochastical environment are simulated with CPN, and the results of simulation are assessed with mathematical statistics, to reflect how the random factors to affect the performance of the protocol.The main innovation of the thesis is as follow, compared to the related research domestic and abroad:(1) Focus on the limitation of Petri net for modeling of complex systems, the thesis proposes the method of modeling hierarchically. Making use of the capability of hierarchical modeling of Colored Petri Net, the logic model of safety communication protocol is established first, then the timed model is established with module of description for time based on the logic model, and finally, module of description for random events is added to reflect the random factors;(2) Against traditional verification methods for communication protocol cannot verify the function, the thesis proposes model checking to verify the function of safety communication protocol. Focuses on the limitation of Petri net for description of sequence of events, the thesis proposes to apply ASK-CTL, supported by Colored Petri Net, to implement model checking for logic of safety communication protocol;(3) Against model checking cannot represent specific performance, the thesis proposes simulation to obtain the performance of safety communication protocol by Colored Petri Net, and assess the simulation results through mathematical statistics;(4) Against method of verification for safety-critical system does not consider performance, the thesis proposes combination of model checking and simulation with Colored Petri Net, to implement the verification of safety communication protocol for both function and performance.The thesis ends with an accomplishment of the verification for the safety communication protocol in the Communication Based Train Control system (CBTC). Model checking with ASK-CTL and simulation with Colored Petri Net are used to verify the function and performance of the protocol, which could not only prove the rationality of the verification method in the thesis, but also guide the development of the protocol.