The Maeslant Barrier Locomobile software controls the barrier arms of the Maeslant storm surge barrier. The actual software controller of the locomobile has been literally modelled in mCRL2. The software was described in a document of over 500 pages. Subsequently, 17 properties have been extracted from the documentation of Rijkswaterstaat, modelled as modal formulas verified on the model. The verification includes the full behaviour, including well defined erroneous behaviour, for instance due to faulty sensors, except for a limited number of situations that caused the statespace to grow too much.

This project clearly shows that it is possible to verify actual control software that occur storm barriers.