A Complete Formal Specification and Verification of the BESW software control system of the Maeslant Storm Surge Barrier

TL;DR

The paper addresses formally specifying and verifying BesW, the Besl (control) software for the Maeslant Storm Surge Barrier, a large-scale and safety-critical system. It translates the DSO-based design into an mCRL2 model of about $5{,}000$ lines, with a state space of $4.98*10^{14}$, and verifies $40$ modal μ-calculus properties, demonstrating feasibility even under fault and testing modes. Key contributions include a complete formal model of BesW, a structured verification workflow, and insights into discrepancies with the original DSO alongside a public discussion of what was validated. The work shows that formal methods can meaningfully support the design and verification of critical infrastructure software, while acknowledging confidentiality constraints and the need for domain-education to broaden adoption.

Abstract

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.

Figures (8)

• Figure 1: The Maeslant Barrier
• Figure 2: The operational processes
• Figure 3: Process modes
• Figure 4: An overview of the control system of the Maeslant Barrier
• Figure 5: Parking dock components