Jan Friso Groote: Specifying the software control of the Prinses Marijke sluice complex


Event Details


The Prinses Marijke Sluizen in Tiel form a part of the Dutch waterways connecting the
river Rhine with the Amsterdam-Rijn kanaal, allowing intense ship traffic while protecting
the hinterland against flooding when water in the Rhine is high.

We made a behavioural model of a controller of this sluice complex including failure of sensors and
actuators and showed that the behaviour is in line with expectations by proving a large number
of properties in the form of modal formulas. This is tricky, as the state space of the controller
is huge (10^18 states). The model is based an SBE model by Ferdi Reijnen,
but deviates from it in a number of interesting aspects. This is work done together with Matthias
Volk.