Formally verifying the correctness of a network-based protocol for railway signalling systems
Jong-Gyu Hwang, J.-H. Lee · WIT transactions on the built environment · 2005
According to the computerization of railway signaling systems, the interface link between the signaling systems has been replaced by the digital communication channel. At the same time, the importance of the communication link is more pronounced than in the past. In this paper, a new network-based protocol for Korean railway signaling has been designed between the CTC and SCADA system, and the overview of the designed protocol is briefly represented. Using an informal method for specifying the communication protocol, a little ambiguity may be contained in the protocol. To clear the ambiguity contained in the designed protocol, we use the LTS model to design the protocol for this interface link between the CTC and SCADA, the LTS is an intermediate model for encoding the operational behavior of processes. Then, we verify automatically and formally the safety and the liveness properties through the model checking method. In particular, the modal u-calculus, which is a highly expressive method of temporal logic, has been applied to the model checking method. It will be expected that the safety, reliability and efficiency of maintenance of the signaling systems will be increased by the use of the designed protocol for railway signalling in Korea. For the covering abstract see ITRD E129315.