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.