Scholarlink

The Maeslant Barrier is a storm surge barrier that protects Rotterdam and its harbour from storm surges in the North Sea. Its software control consists of three major components, one of which is BesW. BesW is responsible for all the movements of the barrier except for pushing and pulling it. In this document, we report on the complete formal specification of BesW in mCRL2. All its behaviour has been specified, including manual and testing modes. Furthermore, all fault situations have been taken into account. The formalisation allows formal verification of all behavioural properties, formulated in the modal \(\mu \) -calculus, with the constraints that water levels only have a restricted number of values and not all combinations of failures of pumps and valves are allowed.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

A Complete Formal Specification and Verification of the BESW Software Control System of the Maeslant Storm Surge Barrier

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Adrian Beers,
  • Jore Booy,
  • Jan Friso Groote,
  • Johan van den Bogaard,
  • Mark Bouwman

摘要

The Maeslant Barrier is a storm surge barrier that protects Rotterdam and its harbour from storm surges in the North Sea. Its software control consists of three major components, one of which is BesW. BesW is responsible for all the movements of the barrier except for pushing and pulling it. In this document, we report on the complete formal specification of BesW in mCRL2. All its behaviour has been specified, including manual and testing modes. Furthermore, all fault situations have been taken into account. The formalisation allows formal verification of all behavioural properties, formulated in the modal \(\mu \) -calculus, with the constraints that water levels only have a restricted number of values and not all combinations of failures of pumps and valves are allowed.