Uitwerkingen Practicum: Spoorwegovergang

PDF versie uitwerkingen

Opgave 1

De trace die Uppaal genereert laat zien dat de trein al bij de overgang kan zijn terwijl die nog niet dicht is. Het probleem is dat de trein in 12 sec bij de overgang kan zijn na de transitie komt!. Maar na de bijbehorende transitie komt? kan de besturing er 1 sec over doen om een signaal omlaag! naar de overgang te sturen, en de overgang kan er vervolgens (in het ergste geval) 15 sec over doen om te sluiten. Aangezien 12 < 15 + 1 gaan het mis. Om het probleem op te lossen kun je

de rekentijd R die de besturing nodig heeft verkleinen (maar dat helpt natuurlijk onvoldoende),
de minimale sluitingstijd S van de overgang verkleinen,
de minimale nadertijd N van de trein vergroten (door de trein langzamer te laten rijden of door de sensor die de komst van de trein detecteert verder weg te zetten).

Om correctheid te garanderen moet gelden dat R+S < N. In het aangepaste model

Overgang_Oplossing1.xml

heb ik in de Declarations sectie expliciet constanten R, S, N ingevoerd, waardoor het eenvoudiger wordt om instanties van het model te testen.

Opgave 2

Ja, er is een probleem. De trein kan direct na een gaat! signaal weer een komt! signaal genereren (bijvoorbeeld wanneer de trein in een rondje rijdt en de sensor die detecteert dat de trein komt vrijwel op dezelfde plek staat als de sensor die detecteert dat de trein gaat). Wanneer echter bij de besturing een signaal binnenkomt dan kan in ons model 1 sec lang geen nieuw signaal worden geaccepteerd. Dit is niet realistisch: in werkelijkheid kan een computer geen signalen "tegenhouden". Ons model is dus niet goed.

We kunnen het probleem oplossen door een extra aanname te maken dat er een minimale tijd D >= 2 verstrijkt tussen het gaan en komen van een trein. Het is dan niet meer mogelijk dat er binnen 1 seconde 2 signalen binnenkomen bij de besturing. Dit kun je eenvoudig bewijzen met Uppaal door een nieuwe toestand Fout toe te voegen waar de besturing naar toe springt wanneer er een signaal binnenkomt als hij aan het rekenen is. Uppaal kan dan bewijzen dat de toestand Fout niet bereikbaar is voor waardes van D groter dan 1. Wanneer D gelijk is aan 0 of 1 dan is Fout wel bereikbaar.

Nog een Probleem

Ook al hebben we het probleem van opgave 2 nu opgelost, toch is het model nog steeds niet goed! Stel dat de trein eerst een gaat! doet en 2 sec later weer een komt!. Weer 1 sec later wil de besturing dan de spoorboom sluiten met een omlaag! opdracht. Maar de overgang zit op dat moment nog steeds in toestand Gaat_open en in die toestand is er geen omlaag? transitie mogelijk! Omdat in Uppaal een omlaag! transitie van een automaat alleen kan plaatsvinden tegelijk/samen met een omlaag? transitie van een andere automaat levert dit een zogenaamde deadlock op, een toestand waarin geen enkele transitie meer mogelijk is. Je kunt deze deadlock ook vinden met behulp van de Uppaal query E<> deadlock. We moeten daarom het model van de overgang uitbreiden en voor iedere toestand aangeven wat er gebeurt wanneer er een omlaag of omhoog instructie binnenkomt. Wanneer we dit doen (op de voor de hand liggende manier waarbij de overgang de ontvangen instructies ook daadwerkelijk uitvoert) dan kan Uppaal bewijzen dat er geen deadlocks meer zijn. De oplossing is uitgewerkt in:

Overgang_Oplossing2a.xml

Overgang_Oplossing2a.q

Wanneer je er goed over nadenkt, dan blijkt de extra aanname dat er minimaal 2 sec zit tussen het gaan en komen van een trein helemaal niet nodig te zijn. We kunnen namelijk ook de besturing aanpassen: wanneer de besturing aan het rekenen is en er komt een nieuw signaal binnen dan wordt uitgegaan van dat nieuwe signaal en het eerdere signaal wordt vergeten. Dus wanneer er bijvoorbeeld eerst een signaal komt dat de trein gaat en direct daarna een signaal dat de trein komt dan zal de besturing opdracht geven om de overgang te sluiten. Deze oplossing is uitgewerkt in:

Overgang_Oplossing2b.xml

Wat deze casus laat zien is dat je nooit blind moet varen op de resultaten van een model checker. Wanneer Uppaal zegt dat een model correct is dan betekent dit nog niet dat het systeem dat je aan het ontwerpen bent ook correct is. Dat is namelijk alleen zo wanneer het model het systeem op een goede manier beschrijft.