在受限工业环境中对 Rijkswaterstaat 隧道控制系统的形式化建模

负责基础设施的荷兰国家机构 Rijkswaterstaat 认识到了形式化建模的重要性，并设立了一个对道路隧道控制进行建模的项目。此举旨在提高隧道控制的标准化程度，并使与供应商的沟通更加顺畅。使用 SysML 的一个子集来构建这些内容庞大的模型。在先前的论文中，我们展示了通过将模型手动转换为 mCRL2，可以使用这些模型来证明行为性质。在本文中，我们报告了向 mCRL2 的自动转换。由于转换结果变得难以处理，我们还研究了在内置验证能力的规范语言 Dezyne 中对隧道控制进行建模，并比较了结果。