Practicum: Flappentapper

Achtergrond

Deze opdracht gaat over de besturingssoftware voor een geldautomaat. Onlangs nog gaf een geldautomaat in de Drentse plaats Vries aan klanten teveel cash. En meer dan 25 miljoen Duitse bankpasjes hebben sinds nieuwjaarsdag 2010 last van een software-bug. Het is dus niet gezegd dat een geldautomaat het altijd goed doet! Doel van deze opdracht is om een eenvoudig model van een geldautomaat te analyseren en te verbeteren. Natuurlijk is het model in deze opdracht een drastische vereenvoudiging van de werkelijkheid!

Instructie

Open de onderstaande files in Uppaal:

Dit model beschrijft een hele simpele versie van een systeem met een klant, een pinautomaat en een bank. 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 je zien als je op het symbooltje links van Klant klikt, en daarna op Declarations.

De klant stopt haar pas in de geldautomaat en doet een verzoek om geld op te nemen. De geldautomaat neemt vervolgens contact op met de bank en vraagt of de klant voldoende saldo heeft. Bij een positief antwoord geeft de geldautomaat eerst geld aan de klant en retourneert daarna de pas. Bij een negatief antwoord wordt de pas teruggegeven aan de klant.

Opgaven

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.)
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.
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
```
gelden.
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 één 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.
Breid het systeem uit zodanig dat de klant ipv geld te vragen ook een vast bedrag – altijd precies een tientje – kan storten.
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 breid 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.)

Producten

Na afloop van het practicum hoef je niets in te leveren, maar laat je Uppaal-modellen wel even aan ons zien. Als het goed is heb je een paar Uppaal-modellen geconstrueerd, met daarbij een argumentatie waarom deze modellen de geformuleerde problemen oplossen.