Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System

Wytse Oortwijn, Marieke Huisman

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)

    Abstract

    Over the last decades, significant progress has been made on formal techniques for software verification. However, despite this progress, these techniques are not yet structurally applied in industry. To reduce the well-known industry–academia gap, industrial case studies are much-needed, to demonstrate that formal methods are now mature enough to help increase the reliability of industrial software. Moreover, case studies also help researchers to get better insight into industrial needs. This paper contributes such a case study, concerning the formal verification of an industrial, safety-critical traffic tunnel control system that is currently employed in Dutch traffic. We made a formal, process-algebraic model of the informal design of the tunnel system, and analysed it using mCRL2. Additionally, we deductively verified that the implementation adheres to its intended behaviour, by proving that the code refines our mCRL2 model, using VerCors. By doing so, we detected undesired behaviour: an internal deadlock due to an intricate, unlucky combination of timing and events. Even though the developers were already aware of this, and deliberately provided us with an older version of their code, we demonstrate that formal methods can indeed help to detect undesired behaviours within reasonable time, that would otherwise be hard to find.

    Original languageEnglish
    Title of host publicationIntegrated Formal Methods
    Subtitle of host publication15th International Conference, IFM 2019, Bergen, Norway, December 2–6, 2019, Proceedings
    EditorsWolfgang Ahrendt, Silvia Lizeth Tapia Tarifa
    PublisherSpringer
    Pages418-436
    Number of pages19
    ISBN (Electronic)978-3-030-34968-4
    ISBN (Print)978-3-030-34967-7
    DOIs
    Publication statusPublished - 2019
    Event15th International Conference on Integrated Formal Methods, IFM 2019 - Western Norway University of Applied Sciences, Bergen, Norway
    Duration: 2 Dec 20196 Dec 2019
    Conference number: 15

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume11918
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference15th International Conference on Integrated Formal Methods, IFM 2019
    Abbreviated titleIFM
    CountryNorway
    CityBergen
    Period2/12/196/12/19

    Fingerprint Dive into the research topics of 'Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System'. Together they form a unique fingerprint.

  • Cite this

    Oortwijn, W., & Huisman, M. (2019). Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System. In W. Ahrendt, & S. L. Tapia Tarifa (Eds.), Integrated Formal Methods: 15th International Conference, IFM 2019, Bergen, Norway, December 2–6, 2019, Proceedings (pp. 418-436). (Lecture Notes in Computer Science; Vol. 11918). Springer. https://doi.org/10.1007/978-3-030-34968-4_23