A Decision-Based Analysis for the Safety Communication Protocol in Train Control System

For safety communication protocol in the train control system, it is necessary for verification to justify why the protocol is to be trusted. Formal methods are powerful specification and verification techniques for establishing high confidence in safety-critical systems. In this paper, the models of safety communication protocol, including the model of state transition, timer and abnormal case in channel, are established by Colored Petri net, which is a known formal tool for modeling. Then, considering the human factors, this paper proposes a decision-based method for supporting verification by analyzing data generated from model of colored Petri net using concept lattice theory and Dempster-Shafer theory, to analyze how the decision of human affect the results of verification. The decision results are reasonable according to general understanding of safety communication protocol, which show that the proposed method could help to gain confidence in the verification process.