International Journal of
Physical Sciences

  • Abbreviation: Int. J. Phys. Sci.
  • Language: English
  • ISSN: 1992-1950
  • DOI: 10.5897/IJPS
  • Start Year: 2006
  • Published Articles: 2572

Full Length Research Paper

Extending promotion to operate controller based on train’s operation

Sher Afzal Khan1*, Nazir Ahmad Zafar2 and Farooq Ahmad1
  1Faculty of Information Technology, University of Central Punjab Lahore, Pakistan. 2Department of Computer Science, College of Computer Science and Information Technology, King Faisal University, Al Hassa, Saudi Arabia.
Email: [email protected]

  •  Accepted: 26 September 2011
  •  Published: 30 November 2011



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.