Real Time Modeling of Automated Interlocking Control System For Passenger Lines of Rawalpindi Cantt Train Station

Abstract

Recent advancements in technology have enabled railway organizations, the world over to shift from manual to computer based automated interlocking systems for increasing their efficiency and profits. Since automated systems are complex and interlocking systems are safety critical systems, these systems should be modeled and verified against safety requirements to weed out any design bugs which might lead to catastrophes during their system life cycles. Timed automata have successfully been used for the modeling and verification of real-time systems. Interlocking is a safety ensuring system whose one application is in railways. A railway interlocking system is the personification of rules which govern the safe movement of any train in a train station. For implementing a software based automated interlocking solution for railway station operations, an error free model is required. In this thesis, we model software based automated interlocking control system of Rawalpindi Cantt (Pakistan) train station using timed automata and verify its correctness using UPPAAL model checking software. The model checker ascertains the absence of errors in a system by inspecting all the possible states or scenarios of the modeled system. By tackling issues of state explosion (uncomputable large number of states) for model checking of large models, we have arrived at a verified modular automated interlocking system design of Rawalpindi Cantt train station. This modular design can easily adapt to the route upgrades and changes within the station by simple variable adjustments and takes a first step in providing an indigenous solution to an indigenous problem of designing an upgraded signaling infrastructure for Pakistan Railway's Rawalpindi Cantt train station.