Automatic Verification of Railway Interlocking Systems: A Case Study

Jakob Lyng Petersen

    Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review

    Abstract

    This paper presents experiences in applying formal verification to a large industrial piece of software. The are of application is railway interlocking systems. We try to prove requirements of the program controlling the Swedish railway Station Alingsås by using the decision procedure which is based on the Stålmarck algorithm. While some requirements are easily proved, others are virtually impossible to manage du to a very large potenbtial state space. We present what has been done in order to get, at least, an idea of whether or not such difficult requirements are fulfilled or not, and we express thoughts on what is needed in order to be able to successfully verify large real-life systems.
    Original languageEnglish
    Title of host publicationProceedings of the Second Workshop on Formal Methods In Software Practice, FMSP'98
    Place of PublicationNew York
    PublisherAssociation of Computing Machinery
    Publication date1998
    Pages1-6
    ISBN (Print)0-89791-954-8
    Publication statusPublished - 1998
    EventSecond Workshop on Second Workshop on Formal Methods In Software Practice, FMSP'98 - Clearwater Beach, Florida, USA
    Duration: 1 Jan 1998 → …

    Conference

    ConferenceSecond Workshop on Second Workshop on Formal Methods In Software Practice, FMSP'98
    CityClearwater Beach, Florida, USA
    Period01/01/1998 → …

    Cite this

    Petersen, J. L. (1998). Automatic Verification of Railway Interlocking Systems: A Case Study. In Proceedings of the Second Workshop on Formal Methods In Software Practice, FMSP'98 (pp. 1-6). Association of Computing Machinery.