Specification and formal verification of safety properties in a point automation system
| Autor: | Ozgur Turay Kaymakci, Ibrahim Sener, Galip Cansever, İlker Üstoğlu |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
0209 industrial biotechnology
Functional verification General Computer Science Computer science Runtime verification 0102 computer and information sciences 02 engineering and technology Petri net Process automation system Formal methods 01 natural sciences Point automation safety formal verification temporal logic timed-arc Petri net Reliability engineering Intelligent verification 020901 industrial engineering & automation 010201 computation theory & mathematics Formal specification Electrical and Electronic Engineering Formal verification |
| Zdroj: | Volume: 24, Issue: 3 1384-1396 Turkish Journal of Electrical Engineering and Computer Science |
| ISSN: | 1303-6203 1300-0632 |
| DOI: | 10.3906/elk-1311-27 |
| Popis: | 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{\i}l Station on the T4 Topkapı-Habibler line, operated by İstanbul Ulaşım A.Ş., as the reference. Moreover, safety requirements for the automation of the points were identified and denoted mathematically while their safety functions were designed. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|