Samenvatting

Het generiek integraal tunnel ontwerp (GITO) bevat generieke modellen voor de besturingssystemen van tunnels van Rijkswaterstaat. Een formele verificatie van deze modellen bevordert de veiligheid en betrouwbaarheid van van GITO afgeleide tunnelcontrolesystemen. De GITO-modellen zijn niet formeel gespecificeerd, wat het gebruik van formele methoden om de juistheid van de modellen te verifiëren bemoeilijkt. In dit rapport wordt onderzocht in hoeverre een formele verificatie van deze modellen mogelijk is.

Er wordt een raamwerk voor formaliseringstransformatie gepresenteerd dat GITO-modellen transformeert naar de formele specificatietaal mCRL2. Deze transformatie wordt toegepast op twee subsystemen van de GITO om de juistheid van de aangeleverde modellen te analyseren. In deze formele analyse worden verschillende tekortkomingen in de specificaties en fouten in de bestaande modellen aan het licht gebracht en worden geverifieerde oplossingen voorgesteld.