The height control of the Elbe Tunnel in Hamburg, Germany, was designed when the fourth tube was added to the tunnel in 2002. Overheight vehicles whose heights exceed four meters are only allowed to use the new tube; otherwise, the vehicle might collide with the ceiling of the tunnel. The height control is responsible for closing the tunnel when it detects that an overheight vehicle tries to enter one of the old tubes. Even though such vehicles are required by law to drive on the right lane and thus a collision should never happen, in reality such laws get ignored occasionally, necessitating a height control in front of the tunnel.

The S# version of the case study can be found here.

The following figure shows a schematic overview of the height control and the road layout. We only consider the two lanes from north (top) to south (bottom), as the tunnel is simply closed whenever an overheight vehicle is detected driving into the other direction. Overall, the height control consists of five sensors: two light barriers lb1 and lb2 as well as three overhead detectors odr, odl, and odf. The sensors are grouped into the pre, main, and end control, with each of the latter two also making use of a timer.

The light barriers span the entire width of both lanes, whereas the overhead detectors are positioned on top of one of the lanes. Consequently, the light barriers can only report that an overheight vehicle passes by, but cannot distinguish between overheight vehicles on the left lane or the right lane; the light barriers cannot be installed in such a way that they observe a single lane only. The overhead detectors, on the other hand, can in fact distinguish between overheight vehicles driving on either of the lanes, but have the disadvantage that they cannot differentiate between overheight vehicles and regular non-overheight ones. By contrast, the light barriers are positioned high enough to ensure that they are only triggered by passing overheight vehicles. The height control therefore has to make use of both types of sensors to determine the positions of overheight vehicles.

When no overheight vehicles are approaching the tunnel, only the pre control is active, that is, the sensors of the main and end controls are deactivated. When lb1 detects an overheight vehicle, the main control is activated, enabling its sensors and starting its timer. Also, an internal counter is increased that counts the number of overheight vehicles that have entered the main control but have yet to leave it. The main control is subsequently deactivated again when an overheight vehicle is reported by lb1 and odr or odl and the counter reaches 0, or the main control's timer times out.

If the main control discovers an overheight vehicle driving on the left lane, the tunnel is closed immediately. Otherwise, the end control is activated, enabling its sensor and starting its timer. When the end control does not detect an overheight vehicle before its timer runs out, it is deactivated; otherwise, the tunnel is closed. The road layout makes it impossible for any vehicle to switch lanes after it has passed odf, but between the last two control stages, vehicles are free to do so.

We consider two kinds of faults for each of the five sensors: Misdetections and false detections. Misdetections are false negatives, that is, a sensor does not report a vehicle passing by that it should detect. False detections, on the contrary, are false positives, so a sensor detects something that is not a vehicle, but, say, a bird.

There are two hazards that are conflicting with each other: On the one hand, the height control is designed to prevent collisions by closing the tunnel whenever an overheight vehicle is about to enter the wrong tube. On the other hand, the height control is also designed to prevent false alarms for economic reasons, as unnecessary closures cause traffic jams. The system design introduced above takes both hazards into account, trying to strike an acceptable balance between collision prevention and false alarms.

Safety analysis reveals that the height control is functionally incorrect due to a design flaw, that is, a collision can happen without the occurrence of any faults. Consequently, design alternatives must be found that fix the problem, while potentially introducing other problems at the same time as well. Any changes to the system design, however, necessitate additional safety analyses. The case study therefore calls for a modeling formalism that conveniently supports models of design alternatives, preferably also allowing for combining different orthogonal design variants. Additionally, the large number of considered faults and the nondeterminism that the vehicles introduce into the model make model checking expensive.