AN AUTOMATIC FORMAL MODEL GENERATION AND VERIFICATION METHOD FOR RAILWAY INTERLOCKING SYSTEMS

Authors : Özgür Turay KAYMAKÇI, Muhammet Ali OZ

Pages : 133-147

View : 13 | Download : 8

Publication Date : 2017-06-19

Article Type : Other Papers

Abstract :Railway transportation systems incorporate many safety critical systems such as signalization systems. Any possible failure within the scope of these safety critical systems can seriously damage nature and lead to human losses. Therefore design, development and implementation of appropriate products have been raised to a certain quality with sector specific standards like EN 50126. Interlocking system is one of the most important and essential product in railway transportation systems. In this paper a new methodology for automatic formal modelling and verification of railway interlocking systems is introduced. Also the developed software automatically generates the formal models of the interlocking system through a visual interface.
Keywords : Formal verification, interlocking, timed arc petri nets, railway signalization systems