Conference paper
Modelling and Verification of Relay Interlocking Systems
Department of Informatics and Mathematical Modeling, Technical University of Denmark1
Software Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark2
Technical University of Denmark3
Department of Electrical Engineering, Technical University of Denmark4
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.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2010 |
Pages: | 141-153 |
Proceedings: | 15th Monterey Workshop |
Series: | Lecture Notes in Computer Science |
Journal subtitle: | Future Trends and Techniques for Development |
ISBN: | 1280386320 , 3642125654 , 3642125662 , 9781280386329 , 9783642125652 and 9783642125669 |
Types: | Conference paper |
DOI: | 10.1007/978-3-642-12566-9_8 |
ORCIDs: | Haxthausen, Anne Elisabeth |
formal methods railway control systems relay interlocking systems software engineering verification
Idle State Model Check Relay System Safety Property Transition Rule