Practicum: Spoorwegovergang in Uppaal

Doel

Ervaring opdoen met een het modelleren en analyseren van systemen met behulp van de model checker Uppaal, te merken dat het maken van (automaten-)modellen eigenlijk helemaal niet moeilijk is, maar dat je voor het maken van goede modellen wel moet nadenken.

Instructie

Computers zijn tegenwoordig onmisbaar bij de besturing van treinen. Maar het blijft moeilijk om de software correct te krijgen! Zo meldt de Vlaamse krant De Standaard in een bericht van 8-1-2010: "Als je met de Thalystrein vanuit Antwerpen Centraal naar Amsterdam wil snellen, moet je er rekening mee houden dat dit staaltje van technologisch vernuft voorbij Antwerpen om de haverklap stilvalt. Zo maar ergens in het veld. De verlichting valt uit, de omroeper vertelt dat de treinbestuurder de computer moet `resetten'. En dat scenario herhaalt zich drie- tot viermaal, tot de grens met Nederland gepasseerd is."

Jullie gaan er voor zorgen dat de besturingssoftware van een spoorwegovergang veilig is. Open het volgende model in Uppaal.

Dit model geeft een sterk vereenvoudigde beschrijving van een spoorwegovergang. Het model bestaat uit drie automaten: een automaat voor een trein, een automaat voor de slagbomen, en een automaat voor de besturing. De file overgang.q bevat een query die uitdrukt dat de spoorbomen dicht zijn wanneer de trein op de overgang is. Een goede manier om inzicht te krijgen in een model is altijd om de simulator te starten!

In het begin is de trein in toestand ver. Dan passeert de trein een sensor en gaat er een signaal komt naar de besturing. Afhankelijk van de snelheid duurt het dan tussen de 12 en 60 sec voordat de trein bij de overgang is. Als de trein voorbij de overgang is dan passeert hij wederom een sensor en gaat er een signaal gaat naar de besturing. De trein is dan weer in toestand ver.

In het begin staan de slagbomen bij de overgang open. Wanneer de overgang een signaal omlaag ontvangt gaan de slagbomen omlaag. Dit duurt maximaal 15 sec. Wanneer de overgang dicht is en er een signaal omhoog arriveert dan gaan de slagbomen weer omhoog. Dit kost tussen de 10 en 20 sec.

Wanneer er een signaal komt arriveert bij de besturing, dan zal die binnen 1 sec een signaal omlaag naar de overgang sturen. En wanneer er een signaal gaat binnenkomt dan zal de besturing binnen 1 sec een signaal omhoog naar de overgang sturen.

Opgave 1

Stel vast met behulp van Uppaal dat de bovengenoemde veiligheids eigenschap niet geldt voor het gegeven model. Genereer een diagnostische trace die dit aantoont. Pas het model aan zodat wel aan de gewenste eigenschap is voldaan. Product: xml file van aangepaste model vergezeld van een toelichting. Wat is er veranderd en waarom is hiermee het probleem opgelost?

Opgave 2

Pas de automaten voor besturing en overgang aan zodat ieder invoersignaal in iedere toestand geaccepteerd wordt: de besturing accepteert in iedere toestand signalen komt en gaat, en de overgang accepteert in iedere toestand signalen omlaag en omhoog. Is het nieuwe model beter dan het oorspronkelijke model? Waarom? Product: toelichting plus xml file van aangepaste model.

Bonusopgave

Pas je model aan voor een situatie waarin er twee treinen zijn die (op verschillende sporen) de kruising kunnen passeren.

Reflectie

Was het gebruik van Uppaal nuttig? Waarom? Wat heb je geleerd?

Producten

Na afloop van het practicum hoef je niets in te leveren. Maar als het goed is heb je een paar Uppaal modellen geconstrueerd, met daarbij een argumentatie waarom deze modellen de geformuleerde problemen oplossen.