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.
