Safety analysis of the height control system for the Elbtunnel

A new tunnel tube crossing the river Elbe has been built in Hamburg until the end of 2002. Therefore, a new height control system was required. A computer examines the signals from light barriers and overhead sensors to detect vehicles, which try to drive into a tube with insufficient height. If necessary, it raises an alarm that blocks the road. This paper describes the application of two safety analysis techniques on this embedded system: model checking has been used to prove functional correctness with respect to a formal model. Fault tree analysis has validated the model and considered technical defects. Their combination uncovered a safety flaw, led to a precise requirement specification for the software, and showed various ways to improve system safety.