Model checking and verification of a rail-side protection system

SARIKOÇ F.

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

  • Publication Type: Article / Article
  • Volume: 244
  • Publication Date: 2025
  • Doi Number: 10.1016/j.scico.2025.103286
  • Journal Name: Science of Computer Programming
  • Journal Indexes: Science Citation Index Expanded (SCI-EXPANDED), Scopus, Academic Search Premier, Applied Science & Technology Source, Compendex, Computer & Applied Sciences, INSPEC, zbMATH
  • Keywords: Fault tree analysis, Formal methods, Model checking, Petri Net, Railway level crossing, Safety verification
  • Erciyes University Affiliated: Yes

Abstract

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.