Abstract

Previous work described by the authors was the use of promotion to link the global state (controller) with the local state (train system). In which the operation of a train makes changes in controller, based on the approach of promotion. However, the model did not apply to any of the critical interlocking components. This paper extends to provide safety along the critical components, that is, when train moves along the straight track or passing through a crossing or level crossing.  For the safety of a train a safe distance (moving block) is associated with every train to avoid collision. Similarly, to define the safe boundaries of crossing and level crossing, circular blocks are defined which has two states, green when it is free and red when it is occupied.  The syntax and type of the formal model is checked by using the Z/EVES tool.

Key words: Formal methods, Z-notation, promotion, moving block railway interlocking, safety properties.