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

Year 2017, Volume: 30 Issue: 2, 133 - 147, 19.06.2017

Özgür Turay Kaymakçı , Muhammet Ali Oz

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

References

• The European Raıl Industry (UNIFE). (2015). Annual Report. Avenue Louise 221, Bte 11 B – 1050 Brussels.
• CENELEC EN 50128, “Railway applications - Communication, Signaling and Processing Systems - Software for Railway Control and Protection Systems (2011).
• S. A. Khan, N. A. Zafar, F. Ahmad, and S. Islam, “Extending Petri net to reduce control strategies of railway interlocking system,” Appl. Math. Model., vol. 38, no. 2, pp. 413–424, 2014.
• H. Wang, F. Schmid, L. Chen, C. Roberts, and T. Xu, “A topology-based model for railway train control systems,” IEEE Trans. Intell. Transp. Syst., vol. 14, no. 2, pp. 819–827, 2013.
• Anne E. Haxthausen, Jan Peleska, and Ralf Pinger, “Applied Bounded Model Checking for Interlocking System Designs,” Towards a Formal Methods Body of Knowledge for Railway Control and Safety Systems: FM-RAIL-BOK Workshop 2013.
• Robert Abo and Laurent Voison, “Data Formal Validation of Railway Safety-Related Systems: Implementing the OVADO Tool,” Towards a Formal Methods Body of Knowledge for Railway Control and Safety Systems: FM-RAIL-BOK Workshop 2013.
• P. James, F. Moller, H. N. Nguyen, M. Roggenbach, S. Schneider, and H. Treharne, “Techniques for modelling and verifying railway interlockings,” Int. J. Softw. Tools Technol. Transf., vol. 16, no. 6, pp. 685–711, 2014.
• Malakar, B., & Roy, B. K. Railway fail-safe signalization and interlocking design based on automation Petri Net. International Conference on Information Communication and Embedded Systems (ICICES), 2014, pp. 1-4.
• Sun, P., Collart-dutilleul, S., & Bon, P. (2015, June). A model pattern of railway interlocking system by Petri nets. International Conference on Models and Technologies for Intelligent Transportation Systems (MT-ITS), 2015, pp. 442-449.
• X. Wang, T. Tang, S. Liu, Study on modeling and verification of CBTC interlocking system. 5th IET International Conference on Wireless, Mobile and Multimedia Networks (ICWMMN), 2013, pp. 350-354.
• I. Sener, O.T. Kaymakçı, I. Ustoğlu, G. Cansever. Specification and formal verification of safety properties in point automation system. Turkish Journal of Electrical and Computer Engineering Sciences, in press, DOI: 10.3906/elk-1311-27.
• M.A.N. Oz, I. Sener, O.T. Kaymakçı, I. Ustoğlu, G. Cansever. Topology based automatic TAPN model generation for railway systems. International Journal of Automation, Mechatronics & Robotics 1 (2014), pp. 6-10.
• M.A.N. Oz, I. Sener, O.T. Kaymakçı, I. Ustoğlu, G. Cansever. A tool for automatic formal modeling of railway interlocking systems. International Conference on Computer as a Tool (EUROCON), 2015, pp. 1-4.
• Andrea Bonacchi, Alessandro Fantechi, Stefano Bacherini, Matteo Tempestini, and Leonardo Cipriani, “Validation of Railway Interlocking Systems by Formal Verification, a Case Study,” Towards a Formal Methods Body of Knowledge for Railway Control and Safety Systems: FM-RAIL-BOK Workshop 2013.
• W. Zheng, C. Liang, R. Wang, and W. Kong, “Automated test approach based on all paths covered optimal algorithm and sequence priority selected algorithm,” IEEE Trans. Intell. Transp. Syst., vol. 15, no. 6, pp. 2551–2560, 2014..
• A. Mekki, M. Ghazel, and A. Toguyéni, “Validation of a New Functional Design of Automatic Protection Systems at Level Crossings with Model-Checking Techniques,” Intell. Transp. Syst. IEEE Trans., vol. 13, no. 2, pp. 714–723, 2012.
• L. Chen, Z. Shan, T. Tang, and H. Liu, “Performance analysis and verification of safety communication protocol in train control system,” Comput. Stand. Interfaces, vol. 33, no. 5, pp. 505–518, 2011.
• A.G. Russo, L. Ladenberger. A formal approach to safety verification of railway signaling systems. Reliability and Maintainability Symposium (RAMS), 2012, pp. 1-4.
• P. James, F. Moller, H.N. Nguyen, M. Roggenbach, S. Schneider, H. Treharne. On modelling and verifying railway interlockings: Tracking train lengths. Science of Computer Programming, Special Issue on Automated Verification of Critical Systems (AVoCS 2012) 96, 2014, pp. 315–336.
• A. Kuzu, O. Songuler, A. Sonat, S. Turk, B. Birol, E. H. Dogruguven. Automatic interlocking table generation from railway topology. IEEE International Conference on Mechatronics, 2011, pp. 64-70.
• U. Yildirim, M. S. Durmus, M. T. Soylemez. Automatic interlocking table generation for railway stations using symbolic algebra. 13th IFAC Symposium on Control in Transportation Systems 13 (2012), 171-176.
• Y. Cao, T. Xu, T. Tang, H. Wang, L. Zhao. Automatic generation and verification of interlocking tables based on domain specific language for computer based interlocking systems (DSL-CBI). IEEE International Conference on Computer Science and Automation Engineering (CSAE) 2 (2011), 511-515.
• L. Jacobsen, M. Jacobsen, M. H. Moller, J. Srba. Verification of timed-arc Petri nets. Lecture Notes in Computer Science 6543 (2011), 46-72.
• M. Andersen, H. G. Larsen, J. Srba, M. G. Sørensen, J. H. Taankvist. Verification of liveness properties on closed timed-arc Petri nets. Lecture Notes in Computer Science 7721 (2013), 69-81.
• A. David, L. Jacobsen, M. Jacobsen, K. Y. Jørgensen, M. H. Møller, J. Srba. TAPAAL 2.0: integrated development environment for timed-arc Petri nets. Lecture Notes in Computer Science 7214 (2012), 492-497.
• E. M. Clarke and E. A. Emerson. Design and synthesis of synchronisation skeletons using branching time temporal logic. In Logic of Programs. Proceedings of Workshop, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer-Verlag, 1981.