@inproceedings{d0d17255002549418cab8c9f8ad2d2e6,
title = "Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment",
abstract = "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. ",
keywords = "Control system, formal specification, tunnel control systems, SysML, mCRL2",
author = "Jilissen, \{Kevin H.J.\} and Peter Dieleman and Groote, \{Jan Friso\}",
year = "2024",
month = mar,
day = "27",
doi = "10.4204/EPTCS.399.6",
language = "English",
volume = "2403.18722",
series = "Electronic Proceedings in Theoretical Computer Science",
publisher = "arXiv.org",
number = "399",
pages = "101--127",
editor = "Fr{\'e}d{\'e}ric Lang and Matthias Volk",
booktitle = "Proceedings Sixth Workshop on Models for Formal Analysis of Real Systems",
}