The verification of railway interlocking systems is a challenging task, and therefore several research groups have suggested to improve this task by using formal methods, but they use different modelling and verification approaches. To advance this research, there is a need to compare these approaches. As a first step towards this, in this paper we suggest a way to compare different formal approaches for verifying designs of route-based interlocking systems and we demonstrate it on modelling and verification approaches developed within the research groups at DTU/Bremen and at Surrey/Swansea. The focus is on designs that are specified by so-called control tables. The paper can serve as a starting point for further comparative studies.
|Title of host publication||Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification|
|Editors||Thierry Lecomte, Ralf Pinger, Alexander Romanovsky|
|Place of Publication||Switzerland|
|ISBN (Print)||978-3-319-33951-1, 978-3-319-33950-4|
|Publication status||Published - 15 Jun 2016|
Bibliographical noteThe full text is not available on the repository.
Haxthausen, A. E., Nguyen, H. N., & Roggenbach, M. (2016). Comparing Formal Verification Approaches of Interlocking Systems. In T. Lecomte, R. Pinger, & A. Romanovsky (Eds.), Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (Vol. 9707, pp. 160-177). Switzerland: Springer Verlag. https://doi.org/10.1007/978-3-319-33951-1_12