Back to Search
Start Over
Specification and Formal Verification of Safety Properties in Point Automation System by Using Timed-Arc Petri Nets
- Source :
- IFAC Proceedings Volumes. 47:12140-12145
- Publication Year :
- 2014
- Publisher :
- Elsevier BV, 2014.
-
Abstract
- In this study, control structure related to the safety of the point automation system, which has a critical significance on tram lines, was designed through Timed-Arc Petri Nets by taking CENELEC 50128 standard as reference. CENELEC 50128 strongly recommends the utilization of Timed-Arc Petri Nets during system modeling (Table A.17) and the utilization of formal proof methods during the verification and test phases of command and control structure developed (Table A.5). The verification was performed through CTL (Computational Tree Logic), which is one of the formal proof methods. Timed-Arc Petri Nets model has been used for the first time in this area through this study. Within this context, the structure was developed by taking the point automation system at the Bastabya Station on T4 Topkapi-Habibler line, operated by Istanbul Ulasim as the reference. Moreover, safety requirements for the automation of the points were identified and denoted mathematically while their safety functions were designed.
- Subjects :
- Computation tree logic
Programming language
business.industry
Computer science
Process architecture
Petri net
Systems modeling
Process automation system
computer.software_genre
Formal methods
Automation
Formal proof
Reliability engineering
Command and control
business
Formal verification
computer
Subjects
Details
- ISSN :
- 14746670
- Volume :
- 47
- Database :
- OpenAIRE
- Journal :
- IFAC Proceedings Volumes
- Accession number :
- edsair.doi...........fc4c2759ef51c84a599040b40b438fa9