Processen/HerkansingPracticum
Herkansing Practicumopdracht: Het Regelen van een OV-Taxi met Semaforen + Analyse van de Oplossing met Uppaal
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 het instappen in een OV-taxi te regelen met behulp van semaforen en je oplossing te modelleren en analyseren met behulp van de model checker Uppaal.
Reizigers op een station komen naar de taxi-standplaats en wachten daar op een OV-taxi. Wanneer een OV-taxi arriveert stappen de wachtende reizigers in. Er is plaats voor maximaal 4 reizigers in een taxi; wanneer er meer dan 4 reizigers staan te wachten zullen sommigen moeten wachten voor de volgende taxi. Wanneer de taxi vol is of alle wachtende reizigers zijn ingestapt kan de taxi vertrekken. Wanneer er geen reizigers zijn zal de taxi direct vertrekken.
Ontwerp met behulp van semaforen een oplossing voor dit probleem (waarbij er een thread is voor iedere taxi en voor iedere reiziger). Beschrijf de oplossing in pseudocode, maak een corresponderend Uppaal model, en toon aan dat je oplossing voldoet aan alle gestelde randvoorwaarden. Je oplossing moet tevens voldoen aan de volgende voorwaarden:
- Afwezigheid van deadlock.
- Afwezigheid van starvation: iedere reiziger die binnenkomt moet uiteindelijk een taxi krijgen, en iedere taxi die aankomt op het station zal daar uiteindelijk ook weer vertrekken.
Instructies
Deze opdracht mag alleen of in groepjes van 2 studenten gemaakt worden. De uiterste inleverdatum is maandag 12 augustus, 23.59uur. Je moet de volgende informatie inleveren (per email bij Frits Vaandrager):
- Een beschrijving van je oplossing in pseudocode (bijvoorbeeld zoals de oplossing van het Bounded-Buffer Producer/Consumer probleem in Figuur 5.13 van Stallings).
- 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!
