Specification and formal verification of safety properties in a point automation system

Abstract

Railroad transportation systems are an area that poses the threat of causing huge risk for both the environment and people if an error emerges during operation. For this reason, designing and developing relevant products in this area is challenging. What is more, methods to be utilized for the purposes of minimizing risk susceptibility are to be specified by international standards. While relevant standards strongly recommend that some methods be utilized based on the desired safety integrity level during the development phase, some methods are not recommended to be utilized. CENELEC 50128 strongly recommends the utilization of timed-arc Petri nets during system modeling and the utilization of formal proof methods during the verification and test phases of the command and control structure developed. In this study, a control structure related to the safety of the point automation system, which has a critical significance for tram lines, was designed through timed-arc Petri nets by taking the relevant standard as the reference. The verification was performed through computational tree logic, which is one of the formal proof methods. The timed-arc Petri nets model has been used for the first time in this area in this study. Within this context, the structure was developed by taking the point automation system at the 50. Yil Station on the T4 Topkapi-Habibler line, operated by Istanbul Ulaşim A.Ş., as the reference. Moreover, safety requirements for the automation of the points were identified and denoted mathematically while their safety functions were designed.