This paper describes how relay interlocking systems as used by the Danish railways can be formally modelled and verified. Such systems are documented by circuit diagrams describing their static layout. It is explained how to derive a state transition system model for the dynamic behaviour of a relay system from such diagrams. Safety properties are identified and formalised as LTL formulae. Model checking is finally used to verify that a model satisfies the safety properties. The method is tested for an existing station in Denmark.
|Title of host publication||Foundations of Computer Software : Future Trends and Techniques for Development.|
|Editors||Christine Choppy, Oleg Sokolsky|
|Number of pages||275|
|Publication status||Published - 2010|
|Event||15th Monterey Workshop - Budapest, Hungary|
Duration: 1 Jan 2008 → …
|Conference||15th Monterey Workshop|
|Period||01/01/2008 → …|
|Series||Lecture Notes in Computer Science|
Bibliographical noteInvited paper.
- relay interlocking systems
- formal methods
- railway control systems
- software engineering
Haxthausen, A. E., Bliguet, M. L., & Kjær, A. (2010). Modelling and Verification of Relay Interlocking Systems. In C. Choppy, & O. Sokolsky (Eds.), Foundations of Computer Software: Future Trends and Techniques for Development. (pp. 141-153). Springer. Lecture Notes in Computer Science, No. 6028 https://doi.org/10.1007/978-3-642-12566-9_8