A formal analysis of Dutch Generic Integral Tunnel Design models
The work
| Authors | Kevin Jilissen; Peter Dieleman; Jan Friso Groote |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2023 |
| Citekey | jilissen2023formal |
Where it appeared
| Published in | Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing |
|---|---|
| Publisher | Association for Computing Machinery |
| Pages | 1681--1684 |
Identifiers
| DOI | 10.1145/3555776.3577786 |
|---|
Access
| Landing page | https://doi.org/10.1145/3555776.3577786 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/3555776.3577786 |
Related
| Distinct from | blom2014vercors |
|---|---|
| Distinct from | blom2017vercors |
| Distinct from | groote2011analyzing |
| Distinct from | groote2021logic |
| Distinct from | madlener2010formal |
| Distinct from | monti2022deductive |
| Distinct from | muller2016viper |
Abstract
The Generic Integral Tunnel Design (GITO) contains generic models for the tunnel control systems of Rijkswaterstaat, part of the Dutch Ministry of Infrastructure and Water Management. A formal verification of these models advances the safety and reliability of GITO derived tunnel control systems. In this paper, the first known large-scale formalisation of tunnel control systems is presented which transforms GITO models to the formal specification language mCRL2. This transformation is applied to two sub-systems of the GITO to analyse the correctness of the supplied models. In this formal analysis, several deficiencies in the specifications and faults in the existing models are revealed and verified solutions are proposed. Some of the presented faults even find their origin in the legally required standards.
A copy is held
pdf, 1.1 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via unpaywall |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-10 14:19 UTC |
Filed under
Cite it as
@inproceedings{jilissen2023formal,
title = {A formal analysis of Dutch Generic Integral Tunnel Design models},
author = {Kevin Jilissen and Peter Dieleman and Jan Friso Groote},
year = {2023},
booktitle = {Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing},
publisher = {Association for Computing Machinery},
pages = {1681--1684},
doi = {10.1145/3555776.3577786},
}
This record lives at https://refs.drheap.org/jilissen2023formal/ and will keep doing so.