Processen/Practicum

Opdracht

De model checker Uppaal is eerder al succesvol ingezet voor het modelleren en analyseren van diverse synchronisatie-problemen, zoals mutual exclusion problemen en problemen die spelen bij het gebruik van semaforen. De opdracht is om het tramverkeer in de Leidsestraat te regelen met behulp van semaforen en je oplossing te modelleren en analyseren met behulp van de model checker Uppaal.

Trams in Amsterdam passeren tussen het Leidseplein en het Koningsplein diverse bruggen over kanalen. Op de bruggen zijn er twee sporen, een voor iedere richting, en haltes waar passagiers kunnen in- en uitstappen. In de winkelstraat tussen de bruggen is er slechts ruimte voor een enkel spoor. De situatie wordt schematisch weergegeven in het onderstaande figuur:

Ontwerp met behulp van semaforen een besturing voor dit systeem (waarbij er voor iedere tram een aparte thread is). Let daarbij op de volgende zaken:

• De bruggen zijn zo kort dat er per richting slechts plaats is voor 1 tram.
• Op het enkele spoor tussen de bruggen passen precies 2 trams.
• Trams kunnen niet van richting veranderen.

Je oplossing moet voldoen aan de volgende voorwaarden:

• Afwezigheid van deadlock.
• Afwezigheid van starvation: iedere tram die binnenkomt moet uiteindelijk het systeem verlaten.

Instructies

Deze opdracht moet gemaakt worden in groepjes van 2 studenten. Mocht je de opdracht alleen willen maken of met meer dan 2 studenten, neem dan eerst even contact op met de docent. De uiterste inleverdatum is maandag 17 juni, 23.59uur. Je moet de volgende informatie inleveren (per email bij Frits Vaandrager):

• De uiteindelijke versies van alle Uppaal modellen die je als onderdeel van de opdracht gemaakt hebt (xml en q files)
• Een uitleg van je oplossing en een toelichting op de modellen. Welke (vereenvoudigende) aannames heb je gemaakt? Tegen welke problemen liep je aan bij het modelleren? Zijn dit goede modellen (hierbij kun je eventueel gebruik maken van een lijst met criteria voor een goed model)?
• Een overzicht van de analyseresultaten die je hebt bereikt met Uppaal. Welke eigenschappen heb je kunnen aantonen? Indien het aantal processen en toestandsvariabelen te groot wordt kan Uppaal modellen vaak niet meer doorrekenen. Speelde dit bij jouw modellen? Zo ja, welke instanties van de modellen konden nog wel worden doorgerekend?
• Een korte reflectie. Wat heb je geleerd bij het maken van deze opdracht?

Tips: Ga uit van een bestaand Uppaal model met semaforen, en gebruik daaruit ihb het template voor semaforen. Wanneer je vast loopt bij het werken aan deze opdracht, schroom dan niet om met je vragen langs te gaan bij de docent!