Formale Modellierung der Rijkswaterstaat-Tunnelsteuerungssysteme in einer eingeschränkten industriellen Umgebung

Die Rijkswaterstaat, die niederländische Behörde für Infrastruktur, hat ein Programm eingerichtet, um die Steuerung von Straßentunneln formal zu modellieren, um die Standardisierung der Tunnelsteuerung zu verbessern und die Kommunikation mit Lieferanten zu erleichtern. Die Autoren untersuchen, wie diese SysML-Modelle automatisch in die formale Spezifikationssprache mCRL2 übersetzt werden können, um formale Verifikation von Sicherheits- und Lebendigkeitseigenschaften durchzuführen. Da die Übersetzung zu unhandlichen Ergebnissen führt, untersuchen sie auch die Modellierung der Tunnelsteuerung in der Spezifikationssprache Dezyne, die integrierte Verifizierungsfähigkeiten hat, und vergleichen die Ergebnisse.