Özgür Turay KAYMAKÇI, Galip CANSEVER, İlker ÜSTOĞLU, İbrahim ŞENER

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

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. Yıl Station on the T4 Topkapı-Habibler line, operated by ˙Istanbul Ula¸sım A.S¸., as the reference. Moreover, safety requirements for the automation of the points were identified and denoted mathematically while their safety functions were designed.

PDF

___

[1] Winter K. Model checking railway interlocking systems. Aust Comp S 2002; 24: 303310.
[2] Kanso K, Moller F, Setzer A. Automated verification of signalling principles in railway interlocking systems. Electronic Notes in Theoretical Computer Science 2009; 250: 1931.
[3] Russo AG, Ladenberger L. A formal approach to safety verification of railway signaling systems. In: Reliability and Maintainability Symposium; 2326 January 2012; Reno, NV, USA. New York, NY, USA: IEEE. pp. 14.
[4] Jo HJ, Hwang JG, Yoon YK. Formal requirements specification in safety-critical railway signaling system. In: Transmission & Distribution Conference & Exposition: Asia and Pacific; 2630 October 2009; Seoul, Korea. New York, NY, USA: IEEE. pp. 14.
[5] Piotrowicz M, Slusarczyk K, Napieralski A. A coloured Petri nets based solution for the generalized railway crossing problem. In: 14th International Conference on Mixed Design of Integrated Circuits and Systems; 2123 June 2007; Ciechocinek, Poland. New York, NY, USA: IEEE. pp. 657660.
[6] Fanti MP, Giua A, Seatzu C. Monitor design for colored Petri nets: an application to deadlock prevention in railway networks. Control Eng Pract 2006; 14: 12311247.
[7] Cheng YH, Yang LA. A fuzzy Petri nets approach for railway traf?c control in case of abnormality: evidence from Taiwan railway system. Expert Syst Appl 2009; 36: 80408048.
[8] Khana SA, Zafar NA, Ahmad F, Islam S. Extending Petri net to reduce control strategies of railway interlocking system. App Math Model 2014; 38: 413424.
[9] Ahmad F, Khan S. Specification and verification of safety properties along a crossing region in a railway network control. App Math Model 2013; 37: 51625170.
[10] Hei X, Takahashi S, Nakamura H. Distributed interlocking system and its safety verification. In: Proceedings of the 6th World Congress on Intelligent Control and Automation, Vol. 2; 2006; Dalian, China. New York, NY, USA: IEEE. pp. 86128615.
[11] Giua A, Seatzu C. Modeling and supervisory control of railway networks using Petri nets. IEEE T Autom Sci Eng 2008; 5: 431445.
[12] Okan MR, Durmu¸s MS, Ozmal K, Ak¸cil L, ¨ Usto˘glu ¨ ˙I, Kaymak¸cı OT. Signaling system solution for urban railways: ¨ Esenler railway depot. In: IFAC Workshop on Advances in Control and Automation Theory for Transportation Applications; 2013.
[13] Mutlu ˙I, Yıldırım U, Durmu¸s MS, S¨oylemez MT. Automatic interlocking table generation for non-ideal railway yards. In: IFAC Workshop on Advances in Control and Automation Theory for Transportation Applications; 2013.
[14] Lozano E, Hernando A, Alonso JA, Laita LM. A logic approach to decision taking in a railway interlocking system using Maple. Math Comput Simulat 2011; 82: 1528.
[15] Kaymak¸cı OT, ¨ Usto˘glu ¨ ˙I, Anık VG. A local modular supervisory controller for a real railway station. In: 5th International System Safety Conference; 1820 October 2010; Manchester, UK. New York, NY, USA: IEEE. pp.16.
[16] CENELEC EN 50128. Railway Applications - Communication, Signalling and Processing Systems - Software for Railway Control and Protection Systems. East Greenwich, RI, USA: Vector Software, 2011.
[17] Jacobsen L, Jacobsen M, Moller MH, Srba J. Verification of timed-arc Petri nets. Lect Notes Comp Sci 2011; 6543: 4672.
[18] Rakkay H., Boucheneb H., Roux OH. Time arc Petri nets and their analysis. In: 9th International Conference on Application of Concurrency to System Design; 13 July 2009; Augsburg, Germany. New York, NY, USA: IEEE.pp. 138147.