This talk describes the experiences that have been obtained with formal methods in the BOS project. The BOS project implements the decision system for the autonomous operation of the storm surge barrier in the Nieuwe Waterweg (New Water Way). CMG Den Haag B.V. designs, implements and installs this system. The BOS (an acronym for its Dutch name 'Beslis & Ondersteunend Systeem') is a decision and support system. This system is designed to autonomously operate the storm surge barrier in the Nieuwe Waterweg. Human intervention is not allowed not in the decision to close the barrier, nor in the closing operation itself. The reason for this is the extreme reliability that is demanded of the system. Dikes in the Netherlands have to have a failure rate of less than one flooding every 10000 years. The artificial barrier, which is built to avoid the massive building of dikes in the urban areas of Rotterdam and Dordrecht, must meet this same failure rate.
Because of the extremely low failure rates that are demanded from the BOS, care must be taken in its design and implementation. One of the approaches used to ensure the reliability of the system is the application of formal methods during the development process. Currently, the design phase has been completed, and the realization of the system has started. This talk summarizes the experiences that were obtained with the application of formal methods during this phase of the project.
Colloquia Series page.