Validation of Railway Interlocking Systems by Formal Verification, A Case Study

被引：6

作者：

Bonacchi, Andrea ^{[1
]}

Fantechi, Alessandro ^{[1
]}

Bacherini, Stefano ^{[2
]}

Tempestini, Matteo ^{[2
]}

Cipriani, Leonardo ^{[2
]}

机构：

[1] Univ Florence, Dipartimento Ingn Informaz, Florence, Italy

[2] Gen Elect Transportat Syst, Florence, Italy

来源：

SOFTWARE ENGINEERING AND FORMAL METHODS | 2014年 / 8368卷

关键词：

D O I：

10.1007/978-3-319-05032-4_18

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Notwithstanding the large amount of attempts to formally verify them, railway interlocking systems still represent a challenging problem for automatic verification. Interlocking systems controlling sufficiently large stations, due to their inherent complexity related to the high number of variables involved, are not readily amenable to automatic verification, typically incurring in state space explosion problems. The study described in this paper aims at evaluating and experimenting the industrial application of verification by model checking for this class of systems. The choices made at the beginning of the study, also on the basis of specific requirements from the industrial partner, are presented, together with the advancement status of the project and the plans for its completion.

引用

页码：237 / 252

页数：16