Topology Based Automatic Formal Model Generation for Point Automation Systems

  • Muhammet Ali Nur Oz Yıldız Technical University, Faculty of Electrical-Electronics, Department of Control and Automation Engineering.
  • Ibrahim Sener Yıldız Technical University, Faculty of Electrical-Electronics, Department of Control and Automation Engineering.
  • Ozgur Turay Kaymakci Yıldız Technical University, Faculty of Electrical-Electronics, Department of Control and Automation Engineering.
  • Ilker Ustoglu Yıldız Technical University, Faculty of Electrical-Electronics, Department of Control and Automation Engineering.
  • Galip Cansever Yıldız Technical University, Faculty of Electrical-Electronics, Department of Control and Automation Engineering.
Keywords: Railway Systems, Automatic model generation, Point automation, Safety, Formal verification, Timed-arc Petri net.

Abstract

Designing and developing a point automation system is a challenging task since railway transportation systems are required to be highly secure and safe systems. Nowadays point automation systems are usually designed manually, this result in a waste of personnel, time and resources. So in this study, we developed and established a software tool in order to automatically generate formal models for point automation systems. The novelty of our study is that our since models are created automatically by a software. Here designing time and human errors are reduced to a minimum thus safe, reliable and secure system models are generated. The developed software has a built in graphical interface which is used to model the basic station topology and using this model, software generates a point automation system’s Timed-Arc Petri Net (TAPN) models, which is a strongly advices formal method by CENELEC EN50128 standard, automatically. Generated TAPN models are also verified automatically for specified safety requirements by using Computational Tree Logic (CTL), which is also a formal proof method strongly advised by CENELEC EN50128 standard. The TAPN models were automatically generated and verified with 100% success by taking the point automation systems of stations on M1 Aksaray-Airport line, operated by Istanbul Transportation Co., as the reference.

DOI: http://dx.doi.org/10.5755/j01.itc.44.1.7382

Author Biographies

Muhammet Ali Nur Oz, Yıldız Technical University, Faculty of Electrical-Electronics, Department of Control and Automation Engineering.

Department of Control and Automation Engineering

Research Assistant

Ibrahim Sener, Yıldız Technical University, Faculty of Electrical-Electronics, Department of Control and Automation Engineering.

Department of Control and Automation Engineering

Research Assistant

Ozgur Turay Kaymakci, Yıldız Technical University, Faculty of Electrical-Electronics, Department of Control and Automation Engineering.

Department of Control and Automation Engineering

Assistant Prof. Dr.

Ilker Ustoglu, Yıldız Technical University, Faculty of Electrical-Electronics, Department of Control and Automation Engineering.

Department of Control and Automation Engineering

Assistant Prof. Dr.

Galip Cansever, Yıldız Technical University, Faculty of Electrical-Electronics, Department of Control and Automation Engineering.

Department of Control and Automation Engineering

Prof. Dr.

Published
2015-03-30
Section
Articles