Model checking water lock systems - presentation by Matthias Volk at STORM_SAFE annual meeting Eindhoven
Matthias Volk of Eindhoven University of Technology (TU/e) demonstrated how model checking can significantly enhance the safety and reliability of water lock control systems. Rather than testing systems only after implementation, model checking enables risks to be identified at an earlier stage, during the design process.
Model checking is an automated verification technique that assesses whether a formal model of a real-world system complies with clearly defined requirements. In this case study, the Princess Marijke lock complex on the Amsterdam–Rijn canal was modelled in detail, including the interaction between two locks and a flood barrier. Safety requirements were expressed using mathematical logic, such as ensuring that lock gates cannot open if paddles on the opposite side are still open.
Using the mCRL2 toolset developed in Eindhoven, all 53 safety requirements were formally verified, even under fault scenarios involving malfunctioning components. The process also revealed gaps in the original specifications, including an absent safety requirement for emergency operation, which was subsequently addressed.
The results highlight the value of model checking: it guarantees correct and safe control behaviour, clarifies requirements and explicitly accounts for component failures. Ultimately, it gives water authorities greater confidence that complex lock systems will operate safely in normal and exceptional conditions.
Matthias Volk
Eindhoven University of Technology