Practicum III: Spoorwegovergang in Uppaal

Practisch

Tijd: 13.45 - 15.45 uur, donderdag 2e week, in HG00.029.
Vanmiddag gaan we in groepjes van twee met Uppaal werken.

Deze informatie staat op http://www.cs.ru.nl/~erikpoll/III/dag9.html

Achtergrond/Relevantie

Model checking is een veelgebruikte techniek die gebruikt wordt ter ondersteuning van het ontwerp en de analyse van computersystemen. Simpel gezegd is een model-checker een computerprogramma dat op een slimme manier alle toestanden van een systeem doorloopt op zoek naar problemen. Vanmiddag gaan we werken met de model-checker Uppaal. (De tool is gratis te downloaden, en draait op elke machine waar Java 1.5 op draait.) Op de Uppaal website moet je nog een onschuldig formuliertje invullen voor je 'm mag downloaden, dus voor het gemak heb ik HIER een lokaal kopietje neergezet.

De model-checker werkt niet met het echte systeem (in ons geval, een echte spoorwegovergang), maar met een abstracte beschrijving van het systeem, wat we het model noemen. Uppaal gebruikt zogenaamde automaten, oftewel toestandsdiagrammen, als modellen.

Naast deze taal (of in dit geval plaatjes) om het systeem te beschrijven is er nog een tweede taal, om de gewenste eigenschappen in op te schrijven. Deze eigenschappen worden queries genoemd.

Doel

Het doel van deze practicumsessie is om hands-on ervaring op te doen met het modelleren en analyseren van systemen met een model-checker (Uppaal), en duidelijk te maken dat het maken van (automaten-)modellen eigenlijk helemaal niet moeilijk is, maar dat je voor het maken van goede modellen toch af en toe echt moet nadenken. Aan het eind van de dag moet je kleine wijzigigen in eenvoudige Uppaal modellen kun maken, op basis van de feedback die de tool je geeft.

Instructie

Opgave 1

Open de onderstaande files in Uppaal. De file overgang.xml beschrijft een sterk vereenvoudigd model van een spoorwegovergang: er is een automaat voor een trein, een automaat voor de slagbomen, en een automaat voor de besturing. Verder bevat de file overgang.q een query die uitdrukt dat de spoorbomen dicht zijn wanneer de trein op de overgang is. Een goede manier om wat inzicht te krijgen in het model is de simulator te starten.
  1. Stel vast met behulp van Uppaal dat de veiligheidseigenschap, geven door de bovengenoemde query, niet geldt voor het gegeven model. Genereer een diagnostische trace die dit aantoont. (Selecteer hiervoor Options -> Diagnostic trace -> Shortest; Modelcheck vervolgens de veiligheidseis met de Verifier, en speel de diagnostische trace daarna na met de Simulator.)

    Pas het model aan zodat wél aan de gewenste eigenschap is voldaan.
    Product: Beschrijf de wijziging in je model. Wat is er veranderd en waarom is hiermee het probleem opgelost? Welk van de componenten (trein, besturing, of overgang) heb je aangepast en waarom lijkt je dit het beste/meest realistische?

  2. Ga na of het systeem kan deadlocken, door de query "A[] not deadlock" te verifiëren. Als er deadlock kan optreden, pas het model dan zodanig aan dat dit niet meer kan. Wat is er veranderd en waarom is hiermee het probleem opgelost?
    Product: Beschrijf de wijziging in je model. Wat is er veranderd en waarom is hiermee het probleem opgelost?

Opgave 2: Flappentapper

Open de onderstaande files in Uppaal Dit modelleert een hele simpele versie van het probleem van de pinautomaat wat vorige week aan bod kwam, waarin we een een klant, een pinautomaat, en een bank modelleren. Er is één Klant, die Klant.geld_op_zak euro op zak heeft, er is één Flappentapper, die Flappentapper.in_kas euro in kas heeft, en er is één Bank, die het saldo van de enige klant administreert. De klant communiceert enkel met de flappentapper, en de flappentapper met de bank. Initiëel heeft de klant 0 euro op zak, staat er 80 euro op haar bankrekening, en zit er 200 euro in de betaalautomaat. Dit kun bijvoorbeeld je zien als je op het symbooltje links van Klant klinkt, en daarna op Declarations.
  1. Verifieer de eigenschappen in flappentapper.q. Probeer het model te verbeteren zodat allebei de eigenschappen waar zijn. (Als het goed is, kom je er hierbij achter dat het model van één van de actoren niet helemaal realistisch was.)

  2. Stel de flappentapper heeft initiëel maar 30 euro in kas. Wat kan er in het model gebeuren, dat in de werkelijk niet realistisch is? Repareer de flappentapper om het model op dit punt te verbeteren.

    Als je dat gedaan hebt, voeg een query toe aan de verifier om te checken of je oplossing werkt. Er mag natuurlijk nog steeds geen deadlock optreden.

  3. Ga na of de eigenschap 
      A[] Klant.geld_op_zak + Bank.saldo == 80
    of de iets zwakkere eigenschap 
      A[] Klant.geld_op_zak + Bank.saldo <= 80
    geldt.

    Denk na wat het gevolg zou zijn als het banksysteem om de een of andere reden crasht op een moment dat deze eigenschappen niet gelden. Kun je begrijpen waarom de bank graag wil dat tenminste een van deze twee eigenschappen geldt?

    Probeer het systeem nu te verbeteren zodanig dat een van de bovenstaande eigenschappen geldt. Denk ook na over de vraag of de wijziging realistisch is.

  4. Breidt het systeem uit zodanig dat de klant ipv geld te vragen ook een vast bedrag - altijd precies een tientje - kan storten.

  5. Stel dat de flappentapper kan crashen vlak voordat-ie wil uitbetalen. Na de crash re-boot de flappentapper, en komt-ie weer terug in de toestand KLAAR. Dit kunnen we modelleren in de flappentapper met een extra pijl van de toestand KLAAR_OM_UIT_TE_BETALEN naar de toestand KLAAR.

    Voeg deze pijl toe, en breidt daarna het model van de flappentapper uit zodat de flappentapper het probleem goed herstelt. De automaat moet na zo'n crash in elk geval de pas teruggeven. Je mag zelf kiezen of de automaat alsnog probeert uit te betalen, of de bank een seintje geeft om de afschrijving ongedaan te maken. (Hint: je kunt een extra variabele in de declaraties van de flappentapper toevoegen waarin die kan zien dat-ie gecrasht is.)

Bonusopgave 3: een race tussen twee processen.

Er zijn twee processen, main and draaiom. Het proces main verhoogt een tellertje count zolang als een Boolean variabele flag op false staat. De enige taak van het proces draaiom is om flag op true te zetten. Als flag true is, dan zal proces main het tellertje count telkens gaan verlagen tot het 0 bereikt, en dan spring het naar zijn eindtoestand. Het proces main verricht zijn acties elke [L1, L2] tijdseenheden, dwz. de tijd tussen twee opeenvolgende acties is minimaal L1 tijdseenheden en maximaal L2 tijdseenheden. Het proces draaiom doet maximaal L tijdseenheden over z'n taak.
  1. Modelleer dit systeem met getimede automaten in Uppaal. Hier alvast een stuk om mee te beginnen is race.xml. De klok tm is bedoeld om de periodes van [L1, L2] tijdseenheden te meten, de klok t is bedoeld om de totale tijd bij te houden.

    NB. Je hebt voor dit model geen kanalen (channels) nodig!

  2. Bedenk een zo nauwkeurig mogelijk bovengrens voor de tijd die main nodig heeft om z'n eindtoestand te bereiken, en valideer deze bovengrens voor een paar mogelijke waardes van L1, L2 en L mbv. Uppaal. Wat voorbeelden van queries, om de syntax te zien, in race.q.

Reflectie

Producten

Voor opgave 2 hoef je niets op papier in te leveren, maar laat je Uppaal modellen even aan ons zien.

Nog wat Uppaal voorbeelden

Hier wat voorbeelden van simpele systemen in Uppaal,