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

Anne Elisabeth Haxthausen, Andreas A. Kjær, Marie Le Bliguet

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    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
    PublisherSpringer
    Publication date2011
    Pages118-132
    ISBN (Print)978-3-642-21436-3
    ISBN (Electronic)978-3-642-21437-0
    DOIs
    Publication statusPublished - 2011
    Event17th International Symposium on Formal Methods (FM 2011) - Limerick, Ireland
    Duration: 20 Jun 201124 Jun 2011
    Conference number: 17

    Conference

    Conference17th International Symposium on Formal Methods (FM 2011)
    Number17
    CountryIreland
    CityLimerick
    Period20/06/201124/06/2011
    SeriesLecture Notes in Computer Science
    Number6664
    ISSN0302-9743

    Fingerprint Dive into the research topics of 'Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems'. Together they form a unique fingerprint.

    Cite this