Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914730476568576 |
|---|---|
| author | Jilissen, Kevin H. J. Dieleman, Peter Groote, Jan Friso |
| author_facet | Jilissen, Kevin H. J. Dieleman, Peter Groote, Jan Friso |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_18722 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment Jilissen, Kevin H. J. Dieleman, Peter Groote, Jan Friso Logic in Computer Science F.4.2; F.4.3; D.2.4 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. |
| title | Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment |
| topic | Logic in Computer Science F.4.2; F.4.3; D.2.4 |
| url | https://arxiv.org/abs/2403.18722 |