Author(s)

J.-G. Hwang & J.-H. Lee

Abstract

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 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 µ-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 signaling in Korea. 1 Introduction There are many computerized equipment in railway signaling systems such as CTC (Centralized Traffic Control) system, EIS (Electronic Interlocking System), ATC (Automation Train Control) system, and LDTS (Local Data Transmission System) and so on. Lots of information is exchanged among the computerized

Keywords