Software Engineering with Formal Methods: The Development of a Storm Surge Barrier Control System - Revisiting Seven Myths of Formal Methods

Jan Tretmans, Klaas Wijbrans, Michel Chaudron

    Research output: Contribution to journalArticleAcademicpeer-review

    17 Citations (Scopus)
    58 Downloads (Pure)

    Abstract

    This paper discusses the use of formal methods in the development of the control system for the Maeslant Kering. The Maeslant Kering is the movable dam which has to protect Rotterdam from floodings while, at (almost) the same time, not restricting ship traffic to the port of Rotterdam. The control system, called BOS, completely autonomously decides about closing and opening of the barrier and, when necessary, also performs these tasks without human intervention. BOS is a safety-critical software system of the highest Safety Integrity Level according to IEC 61508. One of the reliability increasing techniques used during its development is formal methods. This paper reports experiences obtained from using formal methods in the development of BOS. These experiences are presented in the context of Hall's famous “Seven Myths of Formal Methods”.
    Original languageEnglish
    Pages (from-to)195-215
    Number of pages21
    JournalFormal methods in system design
    Volume19
    Issue number2
    DOIs
    Publication statusPublished - 2001

    Fingerprint

    Formal methods
    Surge
    Formal Methods
    Software Engineering
    Software engineering
    Control System
    Control systems
    Movable dams
    Safety-critical Systems
    Flooding
    Ship
    Integrity
    Software System
    Ships
    Safety
    Traffic
    Necessary
    Experience

    Keywords

    • FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS
    • Industrial application of formal methods

    Cite this

    @article{b432e49bafbd441db4f5eb7bbea11d81,
    title = "Software Engineering with Formal Methods: The Development of a Storm Surge Barrier Control System - Revisiting Seven Myths of Formal Methods",
    abstract = "This paper discusses the use of formal methods in the development of the control system for the Maeslant Kering. The Maeslant Kering is the movable dam which has to protect Rotterdam from floodings while, at (almost) the same time, not restricting ship traffic to the port of Rotterdam. The control system, called BOS, completely autonomously decides about closing and opening of the barrier and, when necessary, also performs these tasks without human intervention. BOS is a safety-critical software system of the highest Safety Integrity Level according to IEC 61508. One of the reliability increasing techniques used during its development is formal methods. This paper reports experiences obtained from using formal methods in the development of BOS. These experiences are presented in the context of Hall's famous “Seven Myths of Formal Methods”.",
    keywords = "FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS, Industrial application of formal methods",
    author = "Jan Tretmans and Klaas Wijbrans and Michel Chaudron",
    year = "2001",
    doi = "10.1023/A:1011236117591",
    language = "English",
    volume = "19",
    pages = "195--215",
    journal = "Formal methods in system design",
    issn = "0925-9856",
    publisher = "Springer",
    number = "2",

    }

    Software Engineering with Formal Methods: The Development of a Storm Surge Barrier Control System - Revisiting Seven Myths of Formal Methods. / Tretmans, Jan; Wijbrans, Klaas; Chaudron, Michel.

    In: Formal methods in system design, Vol. 19, No. 2, 2001, p. 195-215.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Software Engineering with Formal Methods: The Development of a Storm Surge Barrier Control System - Revisiting Seven Myths of Formal Methods

    AU - Tretmans, Jan

    AU - Wijbrans, Klaas

    AU - Chaudron, Michel

    PY - 2001

    Y1 - 2001

    N2 - This paper discusses the use of formal methods in the development of the control system for the Maeslant Kering. The Maeslant Kering is the movable dam which has to protect Rotterdam from floodings while, at (almost) the same time, not restricting ship traffic to the port of Rotterdam. The control system, called BOS, completely autonomously decides about closing and opening of the barrier and, when necessary, also performs these tasks without human intervention. BOS is a safety-critical software system of the highest Safety Integrity Level according to IEC 61508. One of the reliability increasing techniques used during its development is formal methods. This paper reports experiences obtained from using formal methods in the development of BOS. These experiences are presented in the context of Hall's famous “Seven Myths of Formal Methods”.

    AB - This paper discusses the use of formal methods in the development of the control system for the Maeslant Kering. The Maeslant Kering is the movable dam which has to protect Rotterdam from floodings while, at (almost) the same time, not restricting ship traffic to the port of Rotterdam. The control system, called BOS, completely autonomously decides about closing and opening of the barrier and, when necessary, also performs these tasks without human intervention. BOS is a safety-critical software system of the highest Safety Integrity Level according to IEC 61508. One of the reliability increasing techniques used during its development is formal methods. This paper reports experiences obtained from using formal methods in the development of BOS. These experiences are presented in the context of Hall's famous “Seven Myths of Formal Methods”.

    KW - FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS

    KW - Industrial application of formal methods

    U2 - 10.1023/A:1011236117591

    DO - 10.1023/A:1011236117591

    M3 - Article

    VL - 19

    SP - 195

    EP - 215

    JO - Formal methods in system design

    JF - Formal methods in system design

    SN - 0925-9856

    IS - 2

    ER -