SavedAdd your journal

Journals / Gazi University Journal of Science / 2017 / Cilt: 30 - Sayı: 2

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

Özgür Turay KAYMAKÇI
Muhammet Ali OZ
Pages
133–147
Publication Date
2017-06-19
DOI
—
🏛️Bibliographic metadata and full text access for this article are provided via DergiPark.
DergiPark Record ↗
✨

AI Summary & Key Takeaways

AI Insight
⚡ TL;DR(Too Long; Didn't Read)

Also the developed software automatically generates the formal models of the interlocking system through a visual interface.

📌 3 Key Takeaways

🎯
Objective & Hypothesis:Railway transportation systems incorporate many safety critical systems such as signalization systems.
📊
Key Findings & Data:Therefore design, development and implementation of appropriate products have been raised to a certain quality with sector specific standards like EN 50126.
💡
Conclusion & Impact:Also the developed software automatically generates the formal models of the interlocking system through a visual interface.
🔬Design:Modeling & Simulation
📍Scope:Comprehensive Sample
⚙️Variables:Formal verification · interlocking · timed arc petri nets

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.

🔖

Cite This Article

KAYMAKÇI, Ö. T., OZ, M. A. (2017). AN AUTOMATIC FORMAL MODEL GENERATION AND VERIFICATION METHOD FOR RAILWAY INTERLOCKING SYSTEMS. Gazi University Journal of Science, Cilt: 30 - Sayı: 2, 133–147. https://ajindex.com/articles/254611

📄 Full Text PDF Viewer

📄

PDF görüntüleyici hazırlanıyor...

References (11)

  1. 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).
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. M.A.N. Oz, I. Sener, O.T. Kaymakçı, I. Ustoğlu, G. Cansever. A tool for automatic formal modeling of rail