Real Time Modeling of Interlocking Control System of Rawalpindi Cantt Train Yard

Interlocking system is a safety critical system which governs the safe movement of trains in a train yard. Recent advancement in technology has enabled railway organizations world over to optimize their operations by using software based automated solutions. Since interlocking systems are not only complex but also safety critical, these systems should be modeled and verified against safety requirements to weed out any design bugs which when discovered during testing or deployment phase in the system life-cycle, will result in high cost overruns and can cause catastrophes. Timed automata have effectively been used for the modeling and verification of real-time safety critical systems. In this paper, we model Rawalpindi Cantt (Pakistan) train yard using timed automata and verify its safety properties using UPPAAL model checker. This verified model can effectively be used to implement the design which will be more reliable as compared to the systems which are verified by classical methods of testing and simulation.