A formal specification of the desired software behaviour of the Princess Marijke lock complex

TL;DR

This paper provides a formal, verifiable specification of the Princess Marijke lock complex's software control system, ensuring safety and reliability through model checking of key requirements.

Contribution

It introduces a concise formal model in mCRL2 for the lock complex's software, serving as a blueprint and verifying 53 safety and correctness properties.

Findings

Formal description in less than 400 lines of mCRL2

Verification of 53 software requirements using model checking

Ensures correctness and safety of the lock complex control software

Abstract

The Princess Marijke lock complex is a large lock and water-protection installation in the Netherlands between the river Rhine and the Amsterdam-Rijnkanaal -- a large waterway connecting the Rhine to the port of Amsterdam. The lock complex consists of two independent locks and a moveable flood-protection barrier. Ensuring safe control of the lock complex is of utmost importance to guarantee both flood-protection and reliable ship operations. This paper gives a precise, formal description of the software control of the lock complex in less than 400 lines of mCRL2 code. This description can act as a blueprint on how the software of this lock complex needs to be constructed. Moreover, using model checking, 53 software requirements are shown to be valid, ensuring that the formal description of the behaviour is correct with regard to these properties and is unlikely to contain mistakes and oversights.