Lessons learned in the application of formal methods to the design of a storm surge barrier control system

The Maeslantkering is a key flood defense infrastructural system in the Netherlands. This movable barrier protects the city and harbor of Rotterdam, without impacting ship traffic under normal circumstances. Its control system, which operates completely autonomously, must be guaranteed to work correctly even under extreme weather conditions, although it closes only sporadically. During its development in the 1990’s, the formal methods Z and Spin were used to increase reliability. As the availability of industrial expert knowledge on these formal methods declines, maintaining the specifications defined back then has become cumbersome. In the quest for an alternative mathematically rigorous approach, this paper reports on an experience in applying supervisory control synthesis. This formal method was recently applied successfully to other types of infrastructural systems like waterway locks, bridges, and tunnels, with the purpose to ensure safe behavior by coordinating hardware components. Here, we show that it can also be used to coordinate several (controller) software systems. Additionally, we compare the lessons learned from the originally used formal methods and link Z to supervisory control synthesis.