Towards the safety properties of moving block railway interlocking system

Nazir Ahmad Zafar, Sher Afzal Khan, Keijiro Araki

Research output: Contribution to journalArticlepeer-review

67 Citations (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.

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

All Science Journal Classification (ASJC) codes

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


Dive into the research topics of 'Towards the safety properties of moving block railway interlocking system'. Together they form a unique fingerprint.

Cite this