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

    380 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, WA, USA
    Duration: 1 Jan 2010 → …

    Conference

    Conference16th Monterey Workshop : Modelling, Development and Verification of Adaptive Systems: the Grand Challenge for Robust Software
    CityMicrosoft Research, Redmond, WA, USA
    Period01/01/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