TY - GEN
T1 - Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations
AU - Macedo, Hugo Daniel dos Santos
AU - Fantechi, Alessandro
AU - Haxthausen, Anne Elisabeth
PY - 2017
Y1 - 2017
N2 - In the railway domain safety is guaranteed by an interlocking system which translates operational decisions into commands leading to field operations. Such a system is safety critical and demands thorough formal verification during its development process. Within this context, our work has focused on the extension of a compositional model checking approach to formally verify interlocking system models for lines with multiple stations. The idea of the approach is to decompose a model of the interlocking system by applying cuts at the network modelling level. The paper introduces an alternative cut (the linear cut) to a previously proposed cut (border cut). Powered with the linear cut, the model checking approach is then applied to the verification of an interlocking system controlling a real-world multiple station line.
AB - In the railway domain safety is guaranteed by an interlocking system which translates operational decisions into commands leading to field operations. Such a system is safety critical and demands thorough formal verification during its development process. Within this context, our work has focused on the extension of a compositional model checking approach to formally verify interlocking system models for lines with multiple stations. The idea of the approach is to decompose a model of the interlocking system by applying cuts at the network modelling level. The paper introduces an alternative cut (the linear cut) to a previously proposed cut (border cut). Powered with the linear cut, the model checking approach is then applied to the verification of an interlocking system controlling a real-world multiple station line.
KW - Railway interlocking
KW - Compositional verification
KW - Model checking
U2 - 10.1007/978-3-319-57288-8_11
DO - 10.1007/978-3-319-57288-8_11
M3 - Article in proceedings
SN - 978-3-319-57287-1
T3 - Lecture Notes in Computer Science
SP - 146
EP - 162
BT - Proceedings of NASA Formal Methods Symposium 2017
PB - Springer
T2 - NASA Formal Methods Symposium 2017
Y2 - 16 May 2017 through 18 May 2017
ER -