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.