Conference paper
Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems
This paper describes a tool for formal modelling relay interlocking systems and explains how it has been stepwise, formally developed using the RAISE method. The developed tool takes the circuit diagrams of a relay interlocking system as input and gives as result a state transition system modelling the dynamic behaviour of the interlocking system, i.e. the dynamic behaviour of the circuits depicted in the diagrams.
The resulting state transition system (model) is expressed in the SAL language such that the SAL model checker can be used to model check required properties of this model of the interlocking system. The tool has been applied to the circuit diagrams of Stenstrup station in Denmark and the resulting formal model has then been model checked to satisfy a number of required safety properties.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2011 |
Pages: | 118-132 |
Proceedings: | 17th International Symposium on Formal Methods (FM 2011) |
Series: | Lecture Notes in Computer Science |
Journal subtitle: | 17th International Symposium on Formal Methods Limerick, Ireland, June 20-24, 2011 Proceedings |
ISBN: | 3642214363 , 3642214371 , 9783642214363 and 9783642214370 |
ISSN: | 03029743 |
Types: | Conference paper |
DOI: | 10.1007/978-3-642-21437-0_11 |
ORCIDs: | Haxthausen, Anne Elisabeth |