DCA - Danish Coastal Authority

The Danish Coastal Authority (Kystdirektoratet) is the official coastal government agency - a division of The Danish Ministry of the Environment and Gender Equality and part of The Environmental Protection Agency. It is as such also adviser for The Danish Minister of the Environment.

The Danish Coastal Authority employs approximately 90 individuals. This workforce includes a variety of professional groups: engineers, surveyors, legal advisors, geologists, biologists, administrative and service personnel.

The Danish Coastal Authority covers all of Denmark’s 7,300 km of coastline, managing the governmental socio-economic interests within the field of coastal protection. The offices is located in Lemvig in Western Jutland. The history of the Danish Coastal Authority dates from as far back as 1868.

The Danish Coastal Authority advise and cooperate with citizens, associations, companies and authorities all over the country, and aim to work nationally and internationally by sharing expertise and by developing joint project for example within the EU. 

The Thorsminde and Hvide Sande drainage sluices were built in 1870 and 1931, respectively. Both sluices have outdated hardware and software systems, making maintenance and climate adaptation increasingly difficult.

The sluices are situated behind a harbour entrance, and normal harbour activities influence the possibilities for draining the fjords – e.g. dredging and navigation can be affected by the current created by the sluices.
Due to climate change, the capacity to drain enough water from the fjords to maintain the water level will be reduced.

The sluices are a barrier to fish migration between the fjord and the sea. In particular, the migration of the European whitefish, the allis shad, and salmon smolt has to be considered when operating the drainage sluice. 

The aim of the case study is to answer the following research questions:

• How the use of data driven models and forecasts for automated sluice control can contribute to improving the conditions for the environment in and around the fjord, without compromising safety and security?
• How to replace and update existing sluice control system in storm surge barriers/sluices with focus on safety and security?
  Two different formal methods are applied and these are outlined below.

AAU models the sluices, their operation, and the surrounding environment as a hybrid system using hybrid automata in Uppaal Stratego. Hybrid automata extend state machines with real valued variables whose evolution is governed by ODEs, enabling accurate modelling of water levels, gate positions, and environmental dynamics. The tool supports controllable and uncontrollable transitions, user defined functions, and stochastic uncertainty, making it suitable for incorporating weather forecasts and unpredictable environmental factors. Moreover, Uppaal allows for the integration of external simulation tools, which enables a richer model closer to the behavior of the real system.

The goal is to synthesize a control program that either autonomously operates the sluices or provides decision support to human operators. Reinforcement learning—specifically Q learning with partition refinement—is used to generate near optimal controllers that optimize behavior over a finite horizon. This results in a model predictive control loop where the controller is periodically re synthesized as conditions change. The learned controller is represented as a decision tree, which can later be minimized for clarity or memory efficiency.

For modelling and validation, AAU collaborates with DCA to construct a detailed model of water levels in Nissum Fjord, Ringkøbing Fjord, and their sluices, using historical data on water levels and wind. Observable variables include water levels, wind speed, and wind direction. The control problem must satisfy several constraints: maintaining safe water levels, respecting salinity requirements (only allowing inflow above 8 m/s wind), enabling fish migration by opening sluices at least four times daily, and limiting gate operations. 

Among all safe controllers, AAU will define an optimization goal—such as minimizing gate movements—to select the preferred solution.

One of the greatest research challenges is to ensure that the system is safe. For instance, it is critical that the water levels are within a given range, but reinforcement learning does not give any guarantees to safety, only expected efficiently. Thus, part of the research will focus on so-called shielded reinforcement learning, where actions leading to an unsafe state somewhere in the future is prohibited. However, the challenge is to compute such a shield.

TU/e applies Synthesis Based Engineering (SBE), a formal method focused on generating supervisory controllers for cyber-physical systems. SBE produces a supervisor that by construction enforces all system requirements while avoiding unnecessary restrictions. The synthesis process is iterative: models are refined, requirements are adjusted, and synthesis is repeated until the resulting supervisor behaves as intended.

Modelling is performed using extended finite automata (EFAs) within Eclipse ESCET, a toolkit for modelling, simulation, and synthesis of supervisory controllers. EFAs provide expressive modelling capabilities while remaining concise, making them suitable for representing the sluice system’s operational logic and constraints. The synthesized supervisor is mathematically guaranteed to satisfy all modelled requirements and to always be able to reach a desired state, eliminating the need for formal verification of the controller itself.

In early stages of development, it is found that the sluice system does not have a constant set of desired states. Based on the environment, the desired states may change. This makes this case different from other infrastructures where SBE has been successfully applied in the past. To capture this in the model, defining different modes of operation is considered.

Validation of the supervisor remains essential: DCA must ensure that the modelled formal requirements and desired states accurately reflect the real system. SBE supports rapid validation through simulation, enabling quick feedback loops and iterative refinement. ESCET can also generate PLC code directly from the synthesized supervisor, allowing practical testing on real hardware.

Unlike AAU’s approach, SBE does not address optimality or provide formal liveness guarantees. Whether a gate eventually opens after being commanded, or whether a controller behaves efficiently, must be determined through simulation and testing rather than formal proof. SBE focuses on correctness with respect to the requirements, leaving performance considerations to empirical evaluation.

Since early 2025, we have been working on analyzing the current sluice operation control system on multiple levels of abstraction. The development of the initial UPPAAL Stratego model has been initialized and the first version of the machine-learning based controller is under development. Also, the development of the Eclipse ESCET model has been initialized and demonstrated for DCA staff. This includes a low-level model of the existing PLC functionality for a single sluice gate as well as a high-level model of the overall functionality of all of the sluice gates based on a number of desired modes of operation. One of the main insights so far is that the current sluice operation instructions leave a lot of space for different interpretations. This can be considered an advantage, but also complicates the optimization of an automatic controller and traceability of the control logic. The use of the two different formal modeling approaches has helped facilitate a fruitful discussion about current sluice operation practice versus other interesting scenarios to investigate with the models.

The main technical, organizational and methodological challenges encountered so far have been: 

• Dealing with multiple desired states (our solution: modes of operation).
• Drafting accurate models of environmental conditions, mainly the salinity.
• Obtaining the correct, precise specifications for a system.
• Identifying and refining the requirements so they can be formally specified is often a lengthy process. Translating numerous written or verbal, naturally phrased requirements into a set of formal, agreed‑upon specifications can take considerable time.

The most important lessons (with respect to these sluices as well as for similar infrastructure projects) learned have been:

• Close communication and short feedback loops have been vital to make significant progress. 
• Defining modes of operation could be a promising way to deal with multi-purpose systems. 
• Simulations are a great way to show the behavior of a (controller) model.

The Danish Coastal Authority expects to gain valuable knowledge by learning from the experiences of other North Sea region partners. In particular, when dealing with software that has reached its end of life, it is important to gain ideas on how to approach the many tasks involved and the overall project.

The sluices may be relatively small constructions, but their operation involves considerable complexity. Universities can help address this complexity through their extensive expertise and knowledge.

• Website