Verifying the accuracy of interlocking tables for railway signalling systems using abstract state machines

ÇELEBİ T., KAYMAKÇI Ö. T.

JOURNAL OF MODERN TRANSPORTATION, cilt.24, sa.4, ss.277-283, 2016 (ESCI) identifier identifier

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 24 Sayı: 4
  • Basım Tarihi: 2016
  • Doi Numarası: 10.1007/s40534-016-0119-1
  • Dergi Adı: JOURNAL OF MODERN TRANSPORTATION
  • Derginin Tarandığı İndeksler: Emerging Sources Citation Index (ESCI), Scopus
  • Sayfa Sayıları: ss.277-283
  • Anahtar Kelimeler: Model checking, Abstract state machines, Interlocking
  • Çanakkale Onsekiz Mart Üniversitesi Adresli: Hayır

Özet

Railway transportation system is a critical sector where design methods and techniques are defined by international standards in order to reduce possible risks to an acceptable minimum level. CENELEC 50128 strongly recommends the utilization of finite statemachines during system modelling stage and formal proof methods during the verification and testing stages of control algorithms. Due to the high importance of interlocking table at the design state of a signalization system, the modelling and verification of interlocking tables are examined in this work. For this purpose, abstract state machines are used as a modelling tool. The developed models have been performed in a generalized structure such that the model control can be done automatically for the interlocking systems. In this study, NuSMV is used at the verification state. Also, the consistency of the developed models has been supervised through fault injection. The developed models and software components are applied on a real railway station operated by Metro Istanbul Co.