up previous Final Report of the COST-247 Action

Use of Formal Methods in The BOS Project

Jan Tretmans

Tele-Informatics and Open Systems Group
Department of Computer Science
University of Twente
P.O. Box 217
7500 AE Enschede, The Netherlands
Email: tretmans@cs.utwente.nl
Tel: +31 53 489 4287
Fax: +31 53 489 3247


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.

This presentation has been given during the COST-247 Project Management Committee Meeting (Stirling, United Kingdom, October 13--14, 1997).

COST-247 Working Group(s): 1

Web Links :

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page