Processen en processoren/Planning/Practica/Practicum 2

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. Allen Downey heeft een leuk boek geschreven over het oplossen van synchronisatie-problemen met behulp van semaforen, The Little Book of Semaphores, hetgeen vrij kan worden gedownload. De opdracht is om een van de synchronisatie-problemen uit Hoofdstukken 4 t/m 7 van dit boek te kiezen, hier een Uppaal model van te maken, en te proberen aan te tonen dat de oplossing van Downey al dan niet correct is. Een paar problemen zijn uitgesloten, aangezien hiervan al Uppaal modellen beschikbaar zijn: het producer/consumer probleem, het dining philosophers probleem, het barbershop probleem en het room-party probleem.

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 dinsdag 14 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 en 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?
• Welke eigenschappen die Downey claimt in zijn boek heb je kunnen analyseren met Uppaal? Welke eigenschappen niet, en waarom? Heb je nog suggesties voor Downey om zijn boek te verbeteren?
• 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!