When a train enters or leaves a railway station, it is important to be sure that it does not derail and does not collide with another train. Therefore, rules have to be made for when a train can enter and leave a station. Like other railway enterprises, Indian Railways uses interlocking systems for ensuring that the safety rules are respected. Such systems are deployed for enforcing these rules on the physical objects of the stations. For instance, the track segments must be aligned correctly in position to make the train to move either straight or turn.
Introduction
A railway station or a railway section is represented as a layout diagram. This layout diagram consists of track segments connected with one another, along with signals, points and level crossings. Signals convey the information regarding operation of train or the track on which the train is set to move, to the driver. Points are the intersection of two track segments. It is used to turn a moving train from main line to loop line. Level Crossings are the control gates that co-ordinate the movement between road transport and railway without collision.
Verification tools can be classified into interactive and automatic tools. Theorem provers, at the current state of art, are not fully automatic for their usual tasks. They are driven through user interaction. As a consequence, experts are needed that are familiar with logic and the particular proof system that underlies the prover. The proof task turns out to be very time and cost intensive if it can be completed at all. Model checking tools, in contrast, do not provide a proof of correctness but rather execute an exhaustive search for errors in the state space of a model. It is an exhaustive test over all possibilities. This search can be done fully automatically. As a result, the user gets an answer that the checked requirement is either satisfied in the model or violated and, in this case, an example shows in which situation the violation may happen.
Many contributions have been made from researchers across the globe with respect to Model checking of Railways interlocking system. But their work is aligned to the Railways System in their country. As the Railways signaling system varies from country to country, it cannot be generalized for all countries. In India, there has been no publications in this field. This is due to the complexity of model checking and unpublished research work for this system.