Rijkswaterstaat, the National Dutch body responsible for infrastructure, recognised the importance of formal modelling and set up a program to model the control of road tunnels. This is done to improve the standardisation of tunnel control and make communication with suppliers smoother. A subset of SysML is used to formulate the models, which are substantial. In an earlier paper we have shown that these models can be used to prove behavioural properties by manually translating the models to mCRL2. In this paper we report on an automatic translation to mCRL2. As the results of the translation became unwieldy, we also investigated modelling tunnel control in the specification language Dezyne which has built-in verification capabilities and compared the results.

翻译：Rijkswaterstaat（荷兰国家基础设施管理机构）认识到正式建模的重要性，并启动了道路隧道控制建模项目。此举旨在提升隧道控制的标准化水平，并优化与供应商的沟通效率。该系统采用SysML子集构建模型（规模庞大）。此前研究已通过人工将模型转换为mCRL2语言，验证了其行为属性。本文则报告了向mCRL2的自动转换方法。由于转换结果变得难以处理，我们进一步研究了在具备内置验证能力的规约语言Dezyne中对隧道控制进行建模，并对两种方案的结果进行了对比分析。