Practicum: Het Alternating Bit Protocol

Dit practicum gaat over het Alternating Bit Protocol (ABP). Dit is een verzameling afspraken voor het versturen van informatie tussen computers in situaties waarbij berichten verloren kunnen gaan. Het ABP is een eenvoudige versie van wat er standaard gebruikt wordt binnen het Internet.

Open de onderstaande files in Uppaal:

Deze files bevatten een model van het ABP. Lees de onderstaande toelichting zorgvuldig en speel wat met de simulator voordat je verder gaat met de opdrachten.

Het Protocol

We nemen aan dat er twee computers zijn, een zender S en een ontvanger R, die elkaar berichten kunnen sturen: via een kanaal K voor berichten van S naar R, en via een kanaal L voor berichten van R naar S:

Bij poort in komen de berichten binnen die S moet versturen. Het is de bedoeling dat al deze berichten in dezelfde volgorde door R worden afgeleverd bij poort out. Maar de kanalen K en L zijn onbetrouwbaar en berichten kunnen verloren raken. De zender stuurt ieder bericht daarom net zo vaak totdat hij een ontvangstbevestiging terugkrijgt via kanaal L. Om te zorgen dat de ontvanger het verschil kan zien tussen een herhaald bericht en een nieuw bericht, voegt de zender aan ieder bericht een extra bit toe. De combinatie van een bericht en zo'n extra bit noemen we een frame. Stel dat S berichten d0, d1, d2, d3,... moet versturen. S stuurt dan eerst net zo lang frames (d0,0) in kanaal K totdat hij een ontvangstbevestiging 0 ontvangt via kanaal L. Dan verstuurt hij net zo lang frames (d1,1) totdat hij een ontvangstbevestiging 1 ontvangt. Vervolgens verstuurt hij net zo lang frames (d2,0) totdat hij weer een ontvangstbevestiging 0 ontvangt. Enzovoorts.

Het Uppaal Model

In ons model nemen we voor het gemak aan dat er slechts twee berichten zijn: 0 en 1. In de begintoestand S0 ontvangt de zender S een nieuw bericht via kanaal in. Als dit bericht 0 is dan springt de zender naar toestand S00 en als het 1 is dan springt de zender naar toestand S10. Vervolgens kunnen er drie dingen gebeuren:

de zender verstuurt het zojuist ontvangen bericht via poort sendframe met een 0 erachter geplakt,
de zender ontvangt een bevestiging 1 via poort receiveack en negeert die, of
de zender ontvangt een bevestiging 0 via poort receiveack en springt naar toestand S1.

In toestand S1 gedraagt de zender zich precies hetzelfde als in toestand S0, alleen is het bit nu geflipt/veranderd.

Automaat K beschrijft een communicatiekanaal waarin 1 frame opgeslagen kan worden. Als er een frame binnenkomt via poort sendframe, dan wordt dit doorgestuurd via poort receiveframe en het kanaal keert terug in de begintoestand. Het is echter ook mogelijk dat het frame verloren gaat: in dat geval keert het kanaal terug naar de begintoestand zonder een frame te versturen. Automaat L is hetzelfde, alleen verstuurt het bits in plaats van frames.

In de begintoestand R0 van de ontvanger kunnen er drie dingen gebeuren:

de ontvanger ontvangt via poort receiveframe een frame dat eindigt met bit 1 en negeert dit,
de ontvanger ontvangt via poort receiveframe een frame dan eindigt met met bit 0 en springt (afhankelijk van het bericht) naar toestand R00 of toestand R10, of
de ontvanger verstuurt een ontvangstbevestiging 1 via poort sendack en blijft in R0.

In de toestanden R00 en R10 verstuurt de ontvanger het zojuist ontvangen bericht via kanaal out en springt vervolgens naar toestand R1. In deze toestand gedraagt de ontvanger zich hetzelfde als in toestand R0, alleen is het bit weer geflipt.

Om aan te tonen dat het ABP berichten altijd goed verstuurt maken we gebruik van een automaat Tester. Deze automaat beschrijft het gedrag van een gebruiker van het ABP die test of het protocol wel goed werkt. De tester stuurt een willekeurig bericht naar poort in en kijkt dan of hetzelfde bericht uit het systeem komt via poort out. Zo ja, dan gaat de tester terug naar de begintoestand en begint overnieuw. Indien er een bericht uit het systeem komt dat er niet is ingestopt dan springt de tester naar toestand ProtocolFout.

Met behulp van Uppaal kun je vaststellen dat de volgende twee eigenschappen gelden:

De tester kan nooit in toestand ProtocolFout komen: A[] not Tester.ProtocolFout.
Het model bevat geen deadlocks: A[] not deadlock.

Vraag 1

Met Uppaal kun je ook laten zien dat het niet mogelijk is om een toestand te bereiken waarin de zender in toestand S0 is en de ontvanger in toestand R1:

not (S.S0 and R.R1)

Anders geformuleerd: als de zender in toestand S0 is (en frames met controlebit 0 gaat versturen) dan weet hij dat de ontvanger niet in toestand R1 kan zijn (waar deze frames juist worden weggegooid). Welke andere combinaties van toestanden van zender en ontvanger zijn verder nog onmogelijk?

Vraag 2

Zoek uit of het ABP nog steeds correct werkt als de kanalen K en L berichten kunnen dupliceren: Pas de automaten voor de twee kanalen aan zodat ieder bericht dat er in wordt gestopt er meerdere keren uit kan komen voordat de automaat terugkeert in zijn begintoestand. Voldoet het aangepaste model nog aan de twee correctheidseigenschappen hierboven? Zo niet, geef dan een tegenvoorbeeld dat laat zien wat er mis kan gaan. Sla je model apart op en lever het in als het practicum is afgelopen.

Vraag 3

Zoek uit of het ABP nog steeds correct werkt indien kanaal K de controlebits kan veranderen (van 1 naar 0 en omgekeerd): Pas automaat K aan zodat dit mogelijk is. Voldoet het aangepaste model nog aan de twee correctheidseigenschappen hierboven? Zo niet, geef dan een tegenvoorbeeld dat laat zien wat er mis kan gaan. Sla je model apart op en lever het in als het practicum is afgelopen.

Vraag 4

Zoek uit of het ABP nog steeds correct werkt indien in kanaal L de controlebits kunnen veranderen. Indien het veranderde ABP niet meer aan de twee correctheidseigenschappen voldoet, geef een tegenvoorbeeld dat laat zien wat er mis kan gaan. Je kunt deze vraag beantwoorden door gewoon na te denken of door gebruik te maken van Uppaal. Om deze vraag met Uppaal te beantwoorden moet de testautomaat aangepast worden. Waarom?