Towards a Framework for Modelling and Verification of Relay Interlocking Systems

Anne Elisabeth Haxthausen (Invited author)

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

    605 Downloads (Pure)

    Abstract

    This paper describes a framework currently under development for modelling, simulation, and verification of relay interlocking systems as used by the Danish railways. The framework is centred around a domain-specific language (DSL) for describing such systems, and provides (1) a graphical editor for creating DSL descriptions, (2) a validator for checking that DSL descriptions are statically well-formed, (3) a graphical simulator for simulating the dynamic behaviour of relay interlocking systems, and (4) verification support for deriving and verifying safety properties of relay interlocking systems. The paper also touches upon how such aframework can be developed using the RAISE Formal Method.
    Original languageEnglish
    Title of host publicationModeling, Development and Verification of Adaptive Systems
    EditorsRadu Calinescu, Ethan Jackson
    Place of PublicationRedmond, Washington, USA
    PublisherMicrosoft Research
    Publication date2010
    Pages101-111
    Publication statusPublished - 2010
    Event16th Monterey Workshop : Modelling, Development and Verification of Adaptive Systems: the Grand Challenge for Robust Software - Microsoft Research, Redmond, United States
    Duration: 31 Mar 20102 Apr 2010
    Conference number: 16

    Conference

    Conference16th Monterey Workshop : Modelling, Development and Verification of Adaptive Systems
    Number16
    LocationMicrosoft Research
    Country/TerritoryUnited States
    CityRedmond
    Period31/03/201002/04/2010

    Bibliographical note

    Invited paper.

    Keywords

    • software engineering, domain-specific language, formal methods, verification, railway control systems, relay interlocking systems, railways

    Fingerprint

    Dive into the research topics of 'Towards a Framework for Modelling and Verification of Relay Interlocking Systems'. Together they form a unique fingerprint.

    Cite this