Akademik Veri Yönetim Sistemi
Uluslararası Bilişim Kongresi 2023(IIC2023) , Batman, Türkiye, 9 - 11 Şubat 2023, ss.100-110
Level
crossings are an essential safety critical component of a railway transportation
system. As time passed, fail-safe software design approaches have been more
widely implemented to replace traditional electromechanical control components.
In this work, we focus on the safety verification work of an automation module
as part of safety-critical system design activities. We designed a Petri net
model for a unidirectional single-line railway section, then we examined the
safety properties of the model by use of formal methods. Later, we employed
linear temporal logic as a specification language and the TINA tool for
exhaustive verification of all executions in the probability space. The
experiment results revealed that the Petri net model with the dedicated case
parameters and assumptions successfully verified the defined safety
requirements.