A Complete Formal Specification and Verification of the BESW software control system of the Maeslant Storm Surge Barrier
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910909235986432 |
|---|---|
| author | Beers, Adrian Booy, Jore Groote, Jan Friso Bogaard, Johan van den Bouwman, Mark |
| author_facet | Beers, Adrian Booy, Jore Groote, Jan Friso Bogaard, Johan van den Bouwman, Mark |
| contents | The Maeslant Barrier is a storm surge barrier that protects Rotterdam and its harbour from storm surges in the North Sea. Its software control consists of three major components, one of which is BesW. BesW is responsible for all the movements of the barrier except for pushing and pulling it. In this document, we report on the complete formal specification of BesW in mCRL2. All its behaviour has been specified, including manual and testing modes. Furthermore, all fault situations have been taken into account. The formalisation allows formal verification of all behavioural properties, formulated in the modal $μ$-calculus, with the constraints that water levels only have a restricted number of values and not all combinations of failures of pumps and valves are allowed. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_08518 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Complete Formal Specification and Verification of the BESW software control system of the Maeslant Storm Surge Barrier Beers, Adrian Booy, Jore Groote, Jan Friso Bogaard, Johan van den Bouwman, Mark Logic in Computer Science The Maeslant Barrier is a storm surge barrier that protects Rotterdam and its harbour from storm surges in the North Sea. Its software control consists of three major components, one of which is BesW. BesW is responsible for all the movements of the barrier except for pushing and pulling it. In this document, we report on the complete formal specification of BesW in mCRL2. All its behaviour has been specified, including manual and testing modes. Furthermore, all fault situations have been taken into account. The formalisation allows formal verification of all behavioural properties, formulated in the modal $μ$-calculus, with the constraints that water levels only have a restricted number of values and not all combinations of failures of pumps and valves are allowed. |
| title | A Complete Formal Specification and Verification of the BESW software control system of the Maeslant Storm Surge Barrier |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.08518 |