A formal analysis of Dutch Generic Integral Tunnel Design models

The work

TitleA formal analysis of Dutch Generic Integral Tunnel Design models
AuthorsKevin Jilissen; Peter Dieleman; Jan Friso Groote
Typeconference paper
Year2023
Citekeyjilissen2023formal

Where it appeared

Published inProceedings of the 38th ACM/SIGAPP Symposium on Applied Computing
PublisherAssociation for Computing Machinery
Pages1681--1684

Identifiers

DOI10.1145/3555776.3577786

Access

Landing pagehttps://doi.org/10.1145/3555776.3577786
Free full texthttps://dl.acm.org/doi/pdf/10.1145/3555776.3577786

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.

Copy held

KindPDF, 1.1 MB
Retrieved2026-08-09
Heldlocal, for personal reference
Where it came fromhttps://dl.acm.org/doi/pdf/10.1145/3555776.3577786

Where this came from

How it got herethe agent went looking · found via unpaywall
First seen2026-08-05
Recordreviewed by a person
Approved2026-08-10

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},
  pages = {1681--1684},
  publisher = {Association for Computing Machinery},
  doi = {10.1145/3555776.3577786},
  url = {https://dl.acm.org/doi/pdf/10.1145/3555776.3577786},
}

This record lives at https://refs.drheap.org/jilissen2023formal/ and will keep doing so.