Princess Marijke 锁 complex 软件行为的形式化规范
系统与控制
2025-07-04 v1 计算机科学中的逻辑
系统与控制
摘要
Princess Marijke 锁 complex 位于荷兰的莱茵河与阿姆斯特丹利茨卡纳尔之间，是一大型闸门和防洪设施，连接莱茵河与阿姆斯特丹港口的大型水路。该锁 complex 由两个独立闸门和一扇可移动防洪闸门组成。确保该锁 complex 的安全控制对于保证防洪和可靠的船舶运营至关重要。本文给出该软件控制的精确、形式化描述，代码不超过 400 行 mCRL2。该描述可作为该锁 complex 软件构造方式的蓝图。此外，通过模型检查，我们验证了 53 项软件需求，确保该行为描述就事论事这些性质，并且不太可能包含错误和遗漏。
引用
@article{arxiv.2507.02721,
title = {A formal specification of the desired software behaviour of the Princess Marijke lock complex},
author = {Jan Friso Groote and Matthias Volk},
journal= {arXiv preprint arXiv:2507.02721},
year = {2025}
}