Model checking and verification of a rail-side protection system

SARIKOÇ F.

Science of Computer Programming, cilt.244, 2025 (SCI-Expanded, Scopus) identifier

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 244
  • Basım Tarihi: 2025
  • Doi Numarası: 10.1016/j.scico.2025.103286
  • Dergi Adı: Science of Computer Programming
  • Derginin Tarandığı İndeksler: Science Citation Index Expanded (SCI-EXPANDED), Scopus, Academic Search Premier, Applied Science & Technology Source, Compendex, Computer & Applied Sciences, INSPEC, zbMATH
  • Anahtar Kelimeler: Fault tree analysis, Formal methods, Model checking, Petri Net, Railway level crossing, Safety verification
  • Erciyes Üniversitesi Adresli: Evet

Özet

Ensuring safe operation of level crossings is crucial in preventing fatalities and injuries at rail-road intersections. This study presents a Petri Net model of a level-crossing system that includes an obstacle detection system and dedicated protection signal to enhance safety. The model was analyzed using linear temporal logic and computation tree logic, with formal verification performed via TINA and TAPAAL tools. As a result of the model-checking experiments, the proposed Petri Net model successfully complies with the given safety criteria. Additionally, Fault Tree Analysis (FTA) was employed to systematically assess system-level risk, highlighting potential failure points and their impact. FTA provides a quantitative risk evaluation that complements the formal verification process, ensuring a thorough system reliability assessment.