Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2011

View graph of relations

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.
Original languageEnglish
Title of host publicationFM 2011: Formal Methods : 17th International Symposium on Formal Methods Limerick, Ireland, June 20-24, 2011 Proceedings
Publication date2011
ISBN (print)978-3-642-21436-3
ISBN (electronic)978-3-642-21437-0
StatePublished - 2011
EventInternational Symposium on Formal Methods - Limerick, Ireland


ConferenceInternational Symposium on Formal Methods
CityLimerick, Ireland
Period01/01/2011 → …
NameLecture Notes in Computer Science
ISSN (Print)0302-9743
CitationsWeb of Science® Times Cited: No match on DOI
Download as:
Download as PDF
Select render style:
Download as HTML
Select render style:
Download as Word
Select render style:

ID: 5868925