A Formal Verification Study on the Rotterdam Storm Surge Barrier
The work
| Title | A Formal Verification Study on the Rotterdam Storm Surge Barrier |
|---|---|
| Authors | Ken Madlener; Sjaak Smetsers; Marko van Eekelen |
| Type | chapter in a collection |
| 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
| Landing page | https://doi.org/10.1007/978-3-642-16901-4_20 |
|---|---|
| Link it arrived with | https://repository.ubn.ru.nl/bitstream/handle/2066/84407/84407.pdf?sequence=1 |
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.
Where this came from
| How it got here | the agent went looking · found via unpaywall |
|---|---|
| First seen | 2026-08-14 |
| Record | reviewed by a person |
| Approved | 2026-08-16 |
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)},
pages = {287--302},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
doi = {10.1007/978-3-642-16901-4_20},
url = {https://doi.org/10.1007/978-3-642-16901-4_20},
}
This record lives at https://refs.drheap.org/madlener2010formal/ and will keep doing so.