Safety Verification of a Transportation Automaton

Creative Commons License

Sarıkoç F.

Uluslararası Bilişim Kongresi 2023(IIC2023) , Batman, Turkey, 9 - 11 February 2023, pp.100-110

  • Publication Type: Conference Paper / Full Text
  • City: Batman
  • Country: Turkey
  • Page Numbers: pp.100-110
  • Erciyes University Affiliated: Yes


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.