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

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

Sayfa
133–147
Yayın Tarihi
2017-06-19
DOI
—
🏛️Bu makalenin bibliyografik verileri ve tam metin bağlantısı DergiPark üzerinden sağlanmıştır.
DergiPark Kaydı ↗
✨

Yapay Zeka Hızlı Bakış & Çıkarımlar

AI Insight
⚡ TL;DR(1 Cümlede Hızlı Çıkarım)

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

📌 3 Maddede Bu Makale

🎯
Amaç & Hipotez:Railway transportation systems incorporate many safety critical systems such as signalization systems.
📊
Temel Bulgular & Veri:Therefore design, development and implementation of appropriate products have been raised to a certain quality with sector specific standards like EN 50126.
💡
Sonuç & Katkı:Also the developed software automatically generates the formal models of the interlocking system through a visual interface.
🔬Tür:Modelleme & Sayısal Simülasyon
📍Kapsam:Genişletilmiş Akademik Örneklem
⚙️Değişkenler: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.

🔖

Bu Makaleye Atıf Yap

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

📄 Tam Metin PDF Okuyucu

📄

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

Kaynakça (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