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

G.J. Tretmans, K.C.J. Wijbrans, M. Chaudron

Research output: Contribution to journalArticle

  • 16 Citations

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��?.
LanguageUndefined
Pages195-215
Number of pages21
JournalFormal methods in system design
Volume19
Issue number2
DOIs
StatePublished - 2001

Keywords

  • FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS
  • EWI-6381

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, EWI-6381",
author = "G.J. Tretmans and K.C.J. Wijbrans and M. Chaudron",
year = "2001",
doi = "10.1023/A:1011236117591",
language = "Undefined",
volume = "19",
pages = "195--215",
journal = "Formal methods in system design",
issn = "0925-9856",
publisher = "Springer Netherlands",
number = "2",

}

Software Engineering with Formal Methods: The Development of a Storm Surge Barrier Control System - Revisiting Seven Myths of Formal Methods. / Tretmans, G.J.; Wijbrans, K.C.J.; Chaudron, M.

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

Research output: Contribution to journalArticle

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,G.J.

AU - Wijbrans,K.C.J.

AU - Chaudron,M.

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 - EWI-6381

U2 - 10.1023/A:1011236117591

DO - 10.1023/A:1011236117591

M3 - Article

VL - 19

SP - 195

EP - 215

JO - Formal methods in system design

T2 - Formal methods in system design

JF - Formal methods in system design

SN - 0925-9856

IS - 2

ER -