Towards the safety properties of moving block railway interlocking system

Nazir Ahmad Zafar, Sher Afzal Khan, Keijiro Araki

研究成果: Contribution to journalArticle

57 引用 (Scopus)


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.

ジャーナルInternational Journal of Innovative Computing, Information and Control
出版物ステータス出版済み - 8 1 2012

All Science Journal Classification (ASJC) codes

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

フィンガープリント Towards the safety properties of moving block railway interlocking system' の研究トピックを掘り下げます。これらはともに一意のフィンガープリントを構成します。

  • これを引用