Towards the safety properties of moving block railway interlocking system

Nazir Ahmad Zafar, Sher Afzal Khan, Keijiro Araki

Research output: Contribution to journalArticle

53 Citations (Scopus)

Abstract

Railway interlocking is a safety critical system because its incorrect functioning may cause serious consequences. Modeling of a reliable interlocking has become a challenging problem due to its inherent complexity and introduction of new technologies. In this paper, formal analysis of safety properties of moving block interlocking is presented preventing collision and derailing of trains at the critical components of the network. We have supposed that the existence of two trains at a component is a collision. If the train's direction and switch control are inconsistent then it is assumed derailing at the switch. A step-by-step procedure is proposed to analyze the safety properties reducing complexity of the system using graph theory and Z notation. Initially, we defined the abstract safety properties, and then they are redefined by introducing a notion of moving block. Further, the safety properties are analyzed and extended by introduction of computer based controls. The formal specification is analyzed and validated using Z/Eves tool.

Original languageEnglish
Pages (from-to)5677-5690
Number of pages14
JournalInternational Journal of Innovative Computing, Information and Control
Volume8
Issue number8
Publication statusPublished - Aug 1 2012

Fingerprint

Railway
Safety
Switch
Collision
Safety-critical Systems
Switches
Formal Analysis
Formal Specification
Graph theory
Inconsistent
Specification languages
Notation
Modeling

All Science Journal Classification (ASJC) codes

  • Software
  • Theoretical Computer Science
  • Information Systems
  • Computational Theory and Mathematics

Cite this

Towards the safety properties of moving block railway interlocking system. / Zafar, Nazir Ahmad; Khan, Sher Afzal; Araki, Keijiro.

In: International Journal of Innovative Computing, Information and Control, Vol. 8, No. 8, 01.08.2012, p. 5677-5690.

Research output: Contribution to journalArticle

Zafar, Nazir Ahmad ; Khan, Sher Afzal ; Araki, Keijiro. / Towards the safety properties of moving block railway interlocking system. In: International Journal of Innovative Computing, Information and Control. 2012 ; Vol. 8, No. 8. pp. 5677-5690.
@article{e95353d5b6c84efabb3f8636b64afa04,
title = "Towards the safety properties of moving block railway interlocking system",
abstract = "Railway interlocking is a safety critical system because its incorrect functioning may cause serious consequences. Modeling of a reliable interlocking has become a challenging problem due to its inherent complexity and introduction of new technologies. In this paper, formal analysis of safety properties of moving block interlocking is presented preventing collision and derailing of trains at the critical components of the network. We have supposed that the existence of two trains at a component is a collision. If the train's direction and switch control are inconsistent then it is assumed derailing at the switch. A step-by-step procedure is proposed to analyze the safety properties reducing complexity of the system using graph theory and Z notation. Initially, we defined the abstract safety properties, and then they are redefined by introducing a notion of moving block. Further, the safety properties are analyzed and extended by introduction of computer based controls. The formal specification is analyzed and validated using Z/Eves tool.",
author = "Zafar, {Nazir Ahmad} and Khan, {Sher Afzal} and Keijiro Araki",
year = "2012",
month = "8",
day = "1",
language = "English",
volume = "8",
pages = "5677--5690",
journal = "International Journal of Innovative Computing, Information and Control",
issn = "1349-4198",
publisher = "IJICIC Editorial Office",
number = "8",

}

TY - JOUR

T1 - Towards the safety properties of moving block railway interlocking system

AU - Zafar, Nazir Ahmad

AU - Khan, Sher Afzal

AU - Araki, Keijiro

PY - 2012/8/1

Y1 - 2012/8/1

N2 - Railway interlocking is a safety critical system because its incorrect functioning may cause serious consequences. Modeling of a reliable interlocking has become a challenging problem due to its inherent complexity and introduction of new technologies. In this paper, formal analysis of safety properties of moving block interlocking is presented preventing collision and derailing of trains at the critical components of the network. We have supposed that the existence of two trains at a component is a collision. If the train's direction and switch control are inconsistent then it is assumed derailing at the switch. A step-by-step procedure is proposed to analyze the safety properties reducing complexity of the system using graph theory and Z notation. Initially, we defined the abstract safety properties, and then they are redefined by introducing a notion of moving block. Further, the safety properties are analyzed and extended by introduction of computer based controls. The formal specification is analyzed and validated using Z/Eves tool.

AB - Railway interlocking is a safety critical system because its incorrect functioning may cause serious consequences. Modeling of a reliable interlocking has become a challenging problem due to its inherent complexity and introduction of new technologies. In this paper, formal analysis of safety properties of moving block interlocking is presented preventing collision and derailing of trains at the critical components of the network. We have supposed that the existence of two trains at a component is a collision. If the train's direction and switch control are inconsistent then it is assumed derailing at the switch. A step-by-step procedure is proposed to analyze the safety properties reducing complexity of the system using graph theory and Z notation. Initially, we defined the abstract safety properties, and then they are redefined by introducing a notion of moving block. Further, the safety properties are analyzed and extended by introduction of computer based controls. The formal specification is analyzed and validated using Z/Eves tool.

UR - http://www.scopus.com/inward/record.url?scp=84865215954&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84865215954&partnerID=8YFLogxK

M3 - Article

VL - 8

SP - 5677

EP - 5690

JO - International Journal of Innovative Computing, Information and Control

JF - International Journal of Innovative Computing, Information and Control

SN - 1349-4198

IS - 8

ER -