Formally Verifying the Correctness of a Network-Based Protocol for Railway Signaling Systems

According to the computerization of railway signaling systems, the interface link between the signaling system 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 the paper, a new network-based protocol for the Korean railway signaling has designed between the CTC and SCADA system, and the overview of the designed protocol is also 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, the paper uses 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 processes. Then, the authors 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.


  • English

Media Info

  • Media Type: Print
  • Features: Figures; References;
  • Pagination: pp 197-206
  • Monograph Title: Urban Transport XI: Urban Transport and the Environment in the 21st Century

Subject/Index Terms

Filing Info

  • Accession Number: 01000977
  • Record Type: Publication
  • ISBN: 184564008X
  • Files: TRIS
  • Created Date: Jun 16 2005 11:06AM