Effective Development and Verification of Railway Control Software

    Research output: Book/ReportReportResearch


    This document presents a method for effective development of software for a product line of similar railway control systems. The software is constructed in three steps: first a specifications in a domain-specific language is created, then a formal behavioural controller model is automatically created from the specification, and finally the model is compiled into executable object code. Formal verification is performed automatically by tools at three levels: (1) the specification is checked to follow the rules of the domain, (2) the controller model is checked to ensure safety, and (3) the object code is verified to be a correct implementation of the controller model.
    Original languageEnglish
    Publication statusPublished - 2011

    Bibliographical note

    This document is a delivery to Rail Net Denmark (Banedanmark) as a part of the Public Sector Consultancy service offered by the Technical University of Denmark.


    Dive into the research topics of 'Effective Development and Verification of Railway Control Software'. Together they form a unique fingerprint.

    Cite this