|Final Report of the COST-247 Action|
Use of Formal Methods in The BOS Project
|Tele-Informatics and Open Systems Group|
|Department of Computer Science|
|University of Twente|
|P.O. Box 217|
|7500 AE Enschede, The Netherlands|
|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.