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

详细信息    查看全文

• 作者：Basri Tugcan Celebi ; Ozgur Turay Kaymakci
• 关键词：Model checking ; Abstract state machines ; Interlocking
• 刊名：Journal of Modern Transportation
• 出版年：2016
• 出版时间：December 2016
• 年：2016
• 卷：24
• 期：4
• 页码：277-283
• 全文大小：518 KB
• 刊物主题：Automotive Engineering; Geoengineering, Foundations, Hydraulics; Regional/Spatial Science;
• 出版者：Springer Berlin Heidelberg
• ISSN：2196-0577
• 卷排序：24

文摘

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 state machines 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.