Towards the formalization of railway interlocking system using Z-notations

Railway interlocking system is a safety critical system. Its malfunction can cause the loss of human life and severe injuries. To remove difficulties from this type of system better and advanced methodologies are required. This paper presents the use of Z-specification to specify the safety properties of the train system. The paper provides division of railway track into sectors and further division into segments. For the safety of the train a safe distance (open block) is associated with trains to avoid collision. Furthermore, this work uses the circular block around the crossing region. The circular block changes its state from green to red whenever it becomes occupied. Moreover the paper also specifies the safety of trains along the linear motion. This work uses the approach of promotion, which provides relation from local to global system. The authors take train as local system and relate it to the whole system through the operation of promotion. The paper also shows how formal methods are used to specify industrial application successfully.