Electronic System Level Design and Verification: Practicum Opdracht 2

Deze pagina is bestemd voor studenten van de Haagse Hogeschool - Faculteit Technologie, Innovatie & Samenleving groep MNES = minor Embedded Systems.

Het is de bedoeling dat je 1 week met deze opdracht bezig bent, 2 uur op het practicum en 2 uur daarbuiten.

Elevator

Het hier gegeven Promela programma modelleert een lift. Dit model is gebaseerd op een model van Gerard Holzmann. Dit model gaat uit van de volgende veronderstellingen:

Er zijn NF verdiepingen (genummerd 0, 1, ... en NF-1) en er is één lift.
De lift wordt door maximaal NP mensen gebruikt. Er is plaats voor iedereen.
Elke verdieping heeft een "vraag"-knop waarmee de lift opgeroepen kan worden.
De lift heeft NF "bestemming"-knoppen waarmee een gebruiker na het instappen de lift naar een bepaalde verdieping kan sturen.
Een druk op een knop wordt gemodelleerd met het versturen van een bericht naar de liftcontroller. De liftcontroller handelt de berichten in FIFO volgorde af.
De controller communiceert met de lift via een netwerk waarin het niet gegarandeerd is dat berichten in dezelfde volgorde aankomen dan ze verzonden zijn. Dit wordt gemodelleerd door de berichten in promela d.m.v. de operator ?? uit te lezen.
Elke globale variabele wordt slecht door 1 proces beschreven, maar kan door meerdere processsen gelezen worden. Om deze reden is het niet nodig de globale variabelen te beveiligen tegen gelijktijdig schrijven door 2 processen..

Bestudeer dit programma en voer een paar random runs uit om te ontdekken hoe dit model werkt. Het is daarbij handig om alleen de output van het model zelf te bekijken. Kies Options, Common, Clear All, OK. Vergroot indien gewenst het aantal stappen m.b.v. de menu optie Settings, Max steps indien nodig.

In de volgende opdrachten wordt aan je gevraagd om bepaalde eigenschappen van het model te bewijzen. Bedenk zelf per eigenschap een effectieve methode. Je kunt gebruik maken van assert statements, progress labels en LTL formules. Het is overigens niet gezegd dat de lift aan de eisen voldoet die je moet bewijzen! Als een bewijs niet geleverd kan worden, verklaar dan duidelijk wat het probleem is en los dit probleem op zodat het gevraagde bewijs wel te geven is.

Opdracht 2a

Bewijs dat het model deadlock vrij is. Zorg ervoor dat de maximale zoekdiepte groot genoeg is. Als dit bewijs niet geleverd kan worden, verklaar dan duidelijk wat het probleem is en los dit probleem op zodat het gevraagde bewijs wel te geven is.

Opdracht 2b

Bewijs dat de lift nooit beweegt met open deuren. Als dit bewijs niet geleverd kan worden, verklaar dan duidelijk wat het probleem is en los dit probleem op zodat het gevraagde bewijs wel te geven is.

Opdracht 2c

Bewijs dat er altijd een gebruiker is die de lift wil gebruiken of gebruikt. Maak daarbij gebruik van het progress label (zie programma). Als een bewijs niet geleverd kan worden, verklaar dan duidelijk wat het probleem is en los dit probleem op zodat het gevraagde bewijs wel te geven is.

Opdracht 2d

Bewijs dat de deur op verdieping X altijd open gaat als de lift op deze verdieping X aankomt. Tip: Je kunt hierbij handig gebruik maken van een logische implicatie. Zie: http://nl.wikipedia.org/wiki/Logische_implicatie. Z'n implicatie kan in een LTL formule worden opgenomen. Bijvoorbeeld: []((oorzaak) -> <> (gevolg)) wat betekent: altijd als oorzaak waar is dan zal ooit/uiteindelijk gevolg waar zijn. Hierbij zijn oorzaak en gevolg proposities (formules die waar of onwaar kunnen zijn). Als je een model op deze LTL formule wilt onderzoeken moet je eerst de LTL formule invoeren in het daarvoor bestemde veld, dan op "Translate" drukken en vervolgens in de dropdownbox waarin standaard "Safety" geselecteerd staat "Acceptance" selecteren en daarna op "Verify" drukken.

Als het je na een half uurtje proberen nog niet is gelukt, dan is hier nog een tip.

Let op! Als het path na de drive letter begint met een hoofdletter U (b.v. H:\User\Harry\Download\elevator.pml) dan geeft spin de foutmelding saw option -f. Dit lijkt me een behoorlijke bug in spin.

Let op! Als je niet alles na de [] tussen haakjes zet dan krijg je altijd 0 errors (met heel veel unreached statements). Dat klopt ook want [](oorzaak) -> iets is altijd true als [](oorzaak) false is. Vergeet die haakjes dus niet!

E studenten die meer willen weten over discrete wiskunde kan ik het gratis boek Logica in Actie van de Open Universiteit aanraden: http://www.ou.nl/Docs/Spinoza/Benthem/LIA_eBook.pdf. De implicatie wordt behandeld in hoofdstuk 2.