Model checking and verification of a rail-side protection system

被引：0
作者：
Sarikoc, Fatih [1 ]
机构：
[1] Erciyes Univ, Fac Engn, Software Engn Dept, Kayseri, Turkiye
来源：
SCIENCE OF COMPUTER PROGRAMMING | 2025年 / 244卷
关键词：
Model checking; Formal methods; Safety verification; Petri Net; Fault tree analysis; Railway level crossing; CRITICAL SCENARIOS; LEVEL-CROSSINGS;
D O I：
10.1016/j.scico.2025.103286
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Ensuring safe operation of level crossings is crucial in preventing fatalities and injuries at railroad 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.
引用
收藏
页数：18
相关论文
共 33 条
  • [1] Ahmad F., 2017, 2017 16 IEEE INT C M
  • [2] [Anonymous], 2005, UIC Code 762
  • [3] Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
  • [4] Berthomieu B, 2006, INT CONF QUANT EVAL, P123
  • [5] Boudnaya J., 2015, SAFETY RELIABILITY C, P1469
  • [6] Byg J, 2009, LECT NOTES COMPUT SC, V5799, P84, DOI 10.1007/978-3-642-04761-9_7
  • [7] Cenelec E., 1999, 50126-Railway Applications: The Specification and Demonstration of Reliability, Availability, Maintainability and Safety (RAMS), V6
  • [8] Clarke E.M., 1981, WORKSHOP LOGIC PROGR
  • [9] E. U. A. f. Railways, 2018, Report on Railway Safety and Interoperability in the EU-2018
  • [10] EC, 2016, Off. J. Eur. Union, V138
1234