A formal analysis of the tunnel control systems of the Rijkswaterstaat GITO

Student thesis: Master

Abstract

The Generic Integral Tunnel Design (GITO) contains generic models for the control systems of Rijkswaterstaat tunnels. A formal verification of these models advances the safety and reliability of GITO derived tunnel control systems. The GITO models are not formally specified, which complicates the use of formal methods to verify the correctness of the models. In this report, the extent to which a formal verification of these models is possible is researched. A formalisation transformation framework 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.
Date of Award29 Aug 2022
Original languageEnglish
SupervisorJan Friso Groote (Supervisor 1) & Peter Dieleman (Supervisor 2)

Cite this

'