Topology Based Automatic Formal Model Generation for Point Automation Systems


Oz M. A. N., Sener I., Kaymakci O. T., Ustoglu I., Cansever G.

INFORMATION TECHNOLOGY AND CONTROL, cilt.44, sa.1, ss.98-111, 2015 (SCI-Expanded) identifier identifier

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 44 Sayı: 1
  • Basım Tarihi: 2015
  • Doi Numarası: 10.5755/j01.itc.44.1.7382
  • Dergi Adı: INFORMATION TECHNOLOGY AND CONTROL
  • Derginin Tarandığı İndeksler: Science Citation Index Expanded (SCI-EXPANDED), Scopus
  • Sayfa Sayıları: ss.98-111
  • Anahtar Kelimeler: Point automation, Timed-arc Petri net, Automatic model generation, Formal verification, Interlocking, Railway systems
  • Yıldız Teknik Üniversitesi Adresli: Evet

Özet

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 results 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 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 recommended 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 recommended 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.