Abstract:

A storm surge barrier is being built near Rotterdam: a movable dam in the Nieuwe Waterweg, the canal connecting Rotterdam with the sea, to protect Rotterdam from being flooded. BOS (in Dutch: Beslis- en Ondersteunend Systeem, i.e., decision and support system) is the computer system that should fully autonomously decide about closing of the barrier and execute the procedure for closing the barrier. CMG Den Haag B.V., responsible for building the software of BOS, decided to use formal methods as one of the means to meet the high safety and reliabilty requirements on BOS. Advised by the University of Twente, CMG selected SPIN/Promela and Z to be used for technical design and validation of the crucial parts of the software. This presentation will report about the experiences with the use of formal methods in the BOS project.