FORMAL VERIFICATION OF PROTOCOL SPECIFIED IN LTS FOR RAILWAY SIGNALING SYSTEMS
Jay H. Lee, Jong-Gyu Hwang, Young-Hyun Yoon, G.T. Park · WIT transactions on the built environment · 2004
This paper describes the designed communication protocol structure for the Korea railway signaling systems and their performance results. The existing communication protocol for signaling contains many critical defects. The novel protocol for signaling is designed to solve these problems. To verify the designed protocol performance on data link control, the simulation is performed on two protocols under the same conditions. From the performance analysis, it is verified that the novel designed protocol has exhibits good performance and also the unquestionable matter are eliminated at the designed protocol formation and mechanism. Using the informal method in specification of the communication protocol, ambiguities are generally contained in the protocol. To clear up the ambiguity contained in the designed protocol, the protocol is specified in LTS and verified through the safety and liveness properties via the model checking method. It is expected that there will be an increase in safety, reliability and efficiency in terms of the maintenance of the signaling system by using the designed novel communication protocol for Korea railway signaling systems.