A Formal Verification Study on the Rotterdam Storm Surge Barrier
The work
| Authors | Ken Madlener; Sjaak Smetsers; Marko van Eekelen |
|---|---|
| Editors | |
| Type | incollection |
| Year | 2010 |
| Citekey | madlener2010formal |
Where it appeared
| Published in | 12th International Conference on Formal Engineering Methods (ICFEM 2010) |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Pages | 287--302 |
Identifiers
| DOI | 10.1007/978-3-642-16901-4_20 |
|---|---|
| OpenAlex | W1544373527 |
Access
| URL | https://repository.ubn.ru.nl/bitstream/handle/2066/84407/84407.pdf?sequence=1 |
|---|---|
| Landing page | https://doi.org/10.1007/978-3-642-16901-4_20 |
Related
| Distinct from | haxthausen2010introduction |
|---|---|
| Distinct from | jilissen2023formal |
| Distinct from | kar2013mosfet |
| Distinct from | monti2022deductive |
Abstract
This paper presents the results of the validation and verification of a crucial component of BOS, a large safety-critical system that decides when to close and open the Maeslantkering, a storm surge barrier near the city of Rotterdam in the Netherlands. BOS was specified in the formal language Z and model checking has been applied to some of its subsystems during its development. A lightweight model of the C++ code and the Z specification of the component was manually developed in the theorem prover PVS. As a result, some essential mismatches between specification and code were identified. We have also validated the Z specification itself by the use of challenge theorems, to assess particular design choices. Tools have been used to exhaustively search for inconsistencies between the original specification and the challenge theorems, which led to deeper issues with the specification itself.
How it got here
| How it got here | agent via unpaywall |
|---|---|
| Added | 2026-08-14 00:00 UTC |
| Approved by | a person 2026-08-16 17:40 UTC |
Filed under
Cite it as
@incollection{madlener2010formal,
title = {A Formal Verification Study on the Rotterdam Storm Surge Barrier},
author = {Ken Madlener and Sjaak Smetsers and Marko van Eekelen},
year = {2010},
booktitle = {12th International Conference on Formal Engineering Methods (ICFEM 2010)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {287--302},
doi = {10.1007/978-3-642-16901-4_20},
}
This record lives at https://refs.drheap.org/madlener2010formal/ and will keep doing so.