Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment

Kevin H. J. Jilissen, Peter Dieleman, Jan Friso Groote

TL;DR

This work addresses the challenge of giving formal semantics to large, semi-formal SysML models of tunnel-control systems to enable verification. It presents an automated translation pipeline from SysML/XMI to $mCRL2$ using Spoofax, augmented by Statix-based typing and Stratego-based AST transformation, and compares this with Dezyne-based verification as a scalable alternative. The results show that while the SysML extension can reproduce verifiable sub-system behavior, the fan-out and state-space explosion (e.g., exceeding $10^8$ outgoing transitions) hinder full-system analysis, whereas Dezyne improves component-level verification but struggles with global properties without extensive decomposition. The study suggests that industrial adoption may benefit from leveraging academically mature formalisms like $mCRL2$ or LOTOS NT and developing workflows that bridge formal verification with commercial modeling tools to manage complexity and maintain traceability.

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.

Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment

TL;DR

This work addresses the challenge of giving formal semantics to large, semi-formal SysML models of tunnel-control systems to enable verification. It presents an automated translation pipeline from SysML/XMI to using Spoofax, augmented by Statix-based typing and Stratego-based AST transformation, and compares this with Dezyne-based verification as a scalable alternative. The results show that while the SysML extension can reproduce verifiable sub-system behavior, the fan-out and state-space explosion (e.g., exceeding outgoing transitions) hinder full-system analysis, whereas Dezyne improves component-level verification but struggles with global properties without extensive decomposition. The study suggests that industrial adoption may benefit from leveraging academically mature formalisms like or LOTOS NT and developing workflows that bridge formal verification with commercial modeling tools to manage complexity and maintain traceability.

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.
Paper Structure (23 sections, 8 equations, 17 figures, 3 tables)

This paper contains 23 sections, 8 equations, 17 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Existing SysML model structure
  3. Model adaptions for formal analysis
  4. Formalising 'structured natural language'
  5. Assignment-based language in SysML
  6. Abstract notation for XMI
  7. Well-typedness using constraint solving in Statix
  8. Leaf Decomposition Layer
  9. Glue Decomposition Layer
  10. Strengths and weaknesses
  11. Alternative models using Dezyne
  12. The pull style model
  13. The push style model
  14. Verification of general properties
  15. Conclusions
  16. ...and 8 more sections

Figures (17)

  • Figure 1: An example of a leaf AD taken from the SysML description of tunnel control systems.
  • Figure 2: An overview of the workflow.
  • Figure 3: Example Activity Diagrams in the newly introduced layers.
  • Figure 4: AST construction from XMI document in Spoofax.
  • Figure 5: A snippet of enum and block definitions in a Block Definition Diagram (BDD) of the model.
  • ...and 12 more figures