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.
-
Availability:
- Find a library where document is available. Order URL: http://worldcat.org/isbn/184564008X
-
Corporate Authors:
Ashurst Lodge
Ashurst, Southampton United Kingdom SO40 7AA -
Authors:
- Hwang, J-G
- Lee, J-H
-
Conference:
- Urban Transport XI: Urban Transport and the Environment in the 21st Century
- Location: Algarve , Portugal
- Date: 2005-4-12 to 2005-4-14
- Publication Date: 2005-3
Language
- 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
- TRT Terms: Computer network protocols; Digital communication systems; Maintenance; Modal analysis; Railroad traffic control; Railroad traffic control devices; Reliability; Safety; Signaling
- Geographic Terms: South Korea
- Subject Areas: Maintenance and Preservation; Operations and Traffic Management; Railroads; Safety and Human Factors;
Filing Info
- Accession Number: 01000977
- Record Type: Publication
- ISBN: 184564008X
- Files: TRIS
- Created Date: Jun 16 2005 11:06AM