Publication: Research - peer-review › Article in proceedings – Annual report year: 2011
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.
|Title of host publication||FM 2011: Formal Methods : 17th International Symposium on Formal Methods Limerick, Ireland, June 20-24, 2011 Proceedings|
|State||Published - 2011|
|Event||International Symposium on Formal Methods - Limerick, Ireland|
|Conference||International Symposium on Formal Methods|
|Period||01/01/2011 → …|
|Name||Lecture Notes in Computer Science|
|Citations||Web of Science® Times Cited: No match on DOI|
Loading map data...