Supervisory Control of a Cyber-Physical System: Storm Surge Barrier

Live Simulation

Interact with the barrier below. The system boots in Automatic Mode — watch the supervisory controller manage the gates, traffic sign, and ship transits as the sea tide rises and falls. Click Switch to Manual to take control yourself; the synthesized supervisor will still enforce every safety requirement.

Abstract

Storm surge barriers protect coastal fjords from flooding during extreme tides while still allowing fresh water to drain and ships to pass through. This project designs a supervisory controller for such a system, inspired by the Hvide Sande barrier in Denmark. The system comprises four gates separating the fjord from the open sea, a rain-fed fjord that must be kept between 1.0m and 4.0m, tidal sea level variation between 0m and 5m, and a canal that allows ships to transit between the two bodies of water under traffic-sign control.

The controller must balance competing objectives: discharge excess fjord water when the sea is lower, close the barrier when the sea rises to critically high levels, sequence ships through the canal safely, and respect the physical constraints of the gate actuators (60 m/s travel speed, 5-second inter-command cooldown to avoid power-grid spikes).

Methodology & Synthesis

The system was originally modeled in CIF 3 (Compositional Interchange Format) within the Eclipse ESCET toolchain. Three layers were modeled separately:

1. Plant (plant.cif) — The uncontrolled physical system as a network of discrete automata: four Gates state machines (bisimulation abstraction with bot/mid/top positions), Sea_level and Fjord_water_level as multi-band state machines, Ships with waiting and transit queues, a Power_management automaton enforcing the 5-second cooldown, and a BoatTimer ensuring ships eventually get priority.

2. Requirements — Seven formal safety specifications expressed as CIF requirement statements:

   • G1: Gates cannot open when sea level is Critically High
   • G2: Gates cannot open from mid→top when fjord level is Normal
   • G3: Gate commands respect the 5-second power cooldown
   • S1: Flow must stay safe (< 200 m³/s) when ships are in the canal
   • S2: Ships can only enter when the traffic sign is Green
   • L1: Fjord level ≤ 4.0m (structural limit)
   • L2: Fjord level ≥ 1.0m (ecological constraint)

3. Supervisor — The supervisor was then mathematically synthesized using cifdatasynth from the Ramadge–Wonham framework. The tool computes the maximally permissive supervisor that enforces all requirements by iteratively restricting each controllable event's guard condition. The resulting plant.ctrlsys.cif contains roughly 1,200 lines of generated boolean logic — every legal combination of plant state in which each controllable event is permitted.

A high-level Automatic_controller was layered on top to implement the operational strategy: open gates sequentially (Gate 1 first, then 2, 3, 4), partially close when the fjord is still high but the sea has risen, fully close when the fjord has drained, and close gates in reverse order when ships need safe flow.

Plant Automata

Each box below is a CIF plant automaton — a discrete abstraction of one physical or logical component of the barrier. Conventions: a double circle marks a location as marked (a valid resting state for the whole system), a stub arrow marks the initial location, solid edges are controllable events (c_…) that the supervisor may fire, and dashed edges are uncontrollable events (u_…) that the environment fires whenever its guard evaluates true. Labels in square brackets are guards; updates follow a slash.

Gates

Bisimulation abstraction of a single gate: three stationary positions (bot, mid, top) and two transit locations. The gate drops into a transit location when the supervisor fires c_open or c_close, and the environment fires the appropriate u_arrived_* once enough simulation time has passed for the actuator to ramp at $3/180\,\text{m/s}$. The plant instantiates four of these as Gate1 … Gate4.

Sea_level

Six-band abstraction of the tide, driven by the sinusoidal sea-level ODE. Every band is a marked location so the supervisor tolerates the sea settling anywhere. Transitions are neighbour-only: the sea cannot jump from Low to High without passing through Normal.

Fjord_water_level

Five bands for the fjord. Unlike the sea, each transition carries a guard so the level only moves when there is a physical cause — rain adding water, or an open gate with an appropriate head difference. Only Low, Normal, and High are marked, which forces the supervisor to keep the fjord out of its critical bands (requirements L1 / L2).

The edge guards reference two shorthand predicates:

Rain

Binary weather plant. Driven by a separate Rain_cycle environment automaton which scripts the tide of wet/dry periods during a simulation run.

Sign

Traffic signal for ships entering the canal. Only Red is marked, so the supervisor is required to bring the sign back to red after every green phase — it cannot leave the canal indefinitely open.

Ships

Single-location plant tracking two bounded counters: q1 (ships waiting at the sign) and q2 (ships currently in the canal), each in $[0, \texttt{maxships}]$ with $\texttt{maxships}=5$. Three self-loops capture the three events — a new ship arriving, a ship being cleared into the canal by the supervisor, and a ship leaving the canal on the fjord side.

BoatTimer

Starvation guard for ships. If a ship has been waiting too long at a red sign, u_timeout moves the plant to HandleShip, where the supervisor is allowed to relax its flow requirements (open a gate even if the fjord is not at the optimal level) in order to let the ship through. This is what lets the system make progress in pathological tide/rain schedules.

Power_management

Enforces the 5-second cooldown between gate actuations (requirement G3). Every c_open or c_close on any gate drops the plant into Cooldown; the environment clears it with u_cooldown_finished once the timer elapses. Only one gate command is permitted per cooldown window, which prevents power-grid spikes from simultaneous actuator draw.

Mode

Operator override. Both u_switch (user clicks the toggle) and u_auto_switch (scripted use-case) flip between Automatic and Manual in either direction. At runtime a Block_auto_switch requirement disables u_auto_switch so only the UI toggle remains active.

ActionButton

Generic button, parametrised by a controllable event c_action and an SVG element id. In Automatic mode the supervisor may fire c_action freely (self-loop on idle); in Manual a UI click raises u_press first, and only then is c_action allowed. The button instances (one per gate command and one for the traffic sign) are what channels operator clicks through the synthesized supervisor so requirements G1–G3 / S1 / S2 remain enforced in manual mode.

Web Architecture — The Hybrid Engine

Porting the Eclipse ESCET simulation to the browser required reimplementing the full hybrid system in TypeScript. The CIF-to-C99 code generator only produces the discrete plant and supervisor — all continuous dynamics (sea tide ODEs, gate actuator ramps, fjord level integration, timers) live in enviroment.cif and are executed by the Eclipse simulator at runtime. For a static web deployment, these had to be rebuilt.

The resulting engine is split into three isolated modules:

1. Continuous Environment (environment.ts) — A numerical integrator for the physical dynamics:

• Sea tide: $l_s(t) = A - A\sin(2\pi t/T + \pi/2)$ with $A = 2.5\,\text{m}$, $T = 43200\,\text{s}$
• Gate actuation: linear ramp ODE $\dot h = \pm v \cdot \mathrm{timeScale}$ at $v = 3/180\,\text{m/s}$
• Fjord level: integrator $\dot h = (Q_\text{rain} + Q_\text{gate} \cdot s)/A_f$ with smooth ±5 cm flow reversal
• Discrete-level detection from continuous values with 5 cm hysteresis

2. Discrete Supervisor (controller.ts) — The FSM cleanly separates two classes of events:

• Uncontrollable events (sea rises, rain starts, ship arrives, boat timeout) fire whenever the environment guard becomes true.
• Controllable events (gate open/close, sign green/red, ship enters) require both the plant precondition and the supervisor invariant to evaluate true. These are grouped into readable guard functions — canOpenGate, canCloseGate, canTurnSignGreen — each annotated with the requirement (G1–G3, S1, S2) it enforces.

3. Simulation Loop (simulation.ts) — A SimulationManager class owns the state and runs a requestAnimationFrame loop. To prevent numerical instability at extreme time-scales (up to 3600×), the integration step is sub-stepped when the effective dt would exceed the solver's maximum step size — mirroring the CIF simulator's --solver-int-maxstep=0.1 setting.

4. SVG DOM Binding (svg-binding.ts) — The original SVG is fetched and injected into the DOM. Every svgout directive from the CIF model becomes a DOM attribute/text update; every svgin directive becomes a click listener wired to a controller command. All button opacity and pointer-events are driven by the same computeButtonStates helper so the UI always reflects exactly which controllable events the supervisor currently permits.

The React wrapper (StormSurgeSimulation.tsx) handles lifecycle management — cancelling the animation frame loop and removing every event listener on unmount — so navigating away from this page leaves no leaked state.

Engineering Takeaways

• Supervisor synthesis as a design tool — rather than hand-writing guard conditions for every legal state, the synthesizer derives them from declarative safety requirements. Translating this cleanly to TypeScript meant mirroring the same declarative approach: requirements at the top of the file, plant preconditions next, synthesized guards as named functions.
• Continuous / discrete separation is a hard boundary — the CIF model keeps these concerns in completely separate files, and the port benefits enormously from maintaining that split. The integrator knows nothing about requirements; the FSM knows nothing about ODEs; they communicate through events.
• Deterministic tick ordering — process uncontrollable events first, then evaluate controllable ones. This ensures the plant state is fully updated before the controller makes decisions, preventing race conditions between simultaneous events.

Technologies Used

CIF 3, Eclipse ESCET, Ramadge–Wonham supervisory control synthesis, TypeScript, React, Next.js, numerical ODE integration, hybrid systems modeling