Formal modelling and verification of interlocking systems featuring sequential release

详细信息    查看全文

• 作者：Linh Hong Vu^a ; ¹ ; ^lvho@dtu.dk ; Anne E. Haxthausen^a ; ¹ ; ^aeha@dtu.dk ; Jan Peleska^b ; ² ; ^{jp@cs.uni-bremen.de}
• 关键词：Railway interlocking systems ; Sequential release ; Formal verification ; Bounded model checking ; k-Induction
• 刊名：Science of Computer Programming
• 出版年：2017
• 出版时间：1 January 2017
• 年：2017
• 卷：133
• 期：part_P2
• 页码：91-115
• 全文大小：1259 K
• 卷排序：133

文摘

A formal model of the ETCS Level 2 compatible interlocking systems. The model accommodates the complexity of the sequential release feature. A scalable verification technique for safety properties for industrial size networks. Experimental verification results for real networks of the Danish Signalling Programme. Benchmarking experiments comparing our BMC approach with other techniques.