Software Engineering with Formal Methods: The Development of a Storm Surge Barrier Control System Revisiting Seven Myths of Formal Methods

摘要

This paper discusses the use of formal methods in the development of the control system for the Maeslant Kering. The Maeslant Kering is the movable dam which has to protect Rotterdam form floodings while, At (almost)the same time, not restricting ship traffic to the port of Rotterdam. The control system, called BOS, Completely autonomously decides about closing and opening of the barrier and, when necessary, also performs These tasks without human intervention.