Promotion of local to global operation in train control system

Railway interlocking system is a safety critical system. Its failure can cause the loss of human life, severe injuries and loss of money. Therefore the complication of this type of system requires advanced methodologies, which provide complete security and quality of a system. One way of achieving this goal is by using formal methods, which are mathematically based languages, techniques and tools used for specifying and verifying such systems. This paper provides the control of trains in a sector of moving block interlocking system using the approach of promotion. The promotion is the approach used to link the local state with a global state in Z specifications. The control comprises three components, i.e. sector, trains and security of a train in a sector.