Formal Verification of a TDMA Protocol Startup Mechanism

Plan

  1. TDMA - stacje i szyna
  2. Synchronizacja stacji
  3. Model - automat z czasem

TDMA - stacje i szyna

TDMA to skrót oznaczający Time Division Multiple Access. Jest to nazwa mechanizmu stosowanego w protokołach komunikacji. Załóżmy, że mamy rozproszone środowisko, w którym kilka stacji komunikuje się między sobą. Medium pośredniczącym jest szyna. Podstawowym założeniem, jest to, że do szyny w jednym momencie może pisać tylko jedna stacja, jeśli chodzi o czytanie to kilka stacji może czytać na raz. Jeśli naraz nastąpi więcej niż jeden zapis do szyny, wszystkie wiadomości uznawane są za popsute (ang. corrupted). W przyszłości zamiast słowa "wiadomość" będziemy używać słowa "ramka".



Dzięki idei TDMA stacje nie przeszkadzają sobie wzajemnie. Jak to działa? Otóż pewien przedział czasu - zwany cyklem komunikacyjnym dzielimy na n równych części (w naszym przypadku, ogólnie te części nie muszą być równe) - n jest liczbą stacji. Każda stacja zna swój przedział czasu i tylko w nim może pisać do szyny. Inne stacje czytają w każdym przedziale, w którym nie wysyłają. Oczywiście stacje muszą mieć zsynchronizowane zegary aby nie przeszkadzały sobie wzajemnie. Co więcej muszą znać wcześniej kolejność.

Synchronizacja stacji

Głównym problemem jest synchronizowanie zegarów. My przyjrzymy się algorytmowi zaproponowanemu przez autorów. Polega on na tym, że jeśli dana stacja jest zsynchronizowana z więcej niż połową stacji to jest wszystko w porządku. Natomiast jeśli stacja nie jest zsynchronizowana z wystarczającą ilością stacji to zmienia ona tryb działania, w którym synchronizuje się ona z poprawnie działającymi stacjami. Jeśli w całym systemie jest mniej niż połowa zsynchronizowanych stacji to przechodzą one do innego trybu działania, w którym wszystkie próbują się zsynchronizować na nowo.

Na czym polega synchronizacja pojedynczej stacji z działającymi?

Stacja przechowuje licznik błędnie odebranych ramek. W tzw. trybie resynchronizacji stacja ta nie może nic wysyłać - dzięki temu nie generuje błędów w innych stacjach. Próbuje ona odebrać przychodzącą ramkę. W momencie startu ramki (SOF - start of frame) ustawia sobie odpowiednio licznik, dzięki czemu jest już zsynchronizowana z jedną stacją. Teraz zgodnie już z nowym zegarem odbiera kolejne ramki dzięki czemu synchronizuje się z coraz większą ilością stacji. Gdy wszystko poszło dobrze i znów jest zsynchronizowana z więcej niż połową stacji wraca do normalnego działania.

Co gdy więcej niż połowa stacji nie jest ze sobą zsynchronizowana?

Widać, że wtedy wszystkie stacje przejdą do trybu resynchronizacji. Lecz wtedy nie ma już poprawnie działających stacji, które wysyłają ramki, przez co stacje nie mogą się zsynchronizować. I na to jest sposób. Każda stacja gdy zobaczy pełen cykl komunikacyjny bez komunikacji przechodzi do tzw. trybu "recovery". W trybie tym ramki funkcjonują podobnie jak w trybie resynchronizacji, tzn. jeśli odbiorą więcej niż połowę poprawnych ramek (co oznacza że są zsynchronizowane z więcej niż połową stacji) to przechodzą do normalnego trybu działania. Tryb "recovery" różni się tym od trybu resynchronizacji, że stacje kolejno wysyłają ramki. Oczywiście jeśli były zdesynchronizowane to dlaczego miałoby się to teraz zmienić?

[Wyjaśnienia na tablicy]

Model - automat z czasem

Mamy dwa automaty - jeden reprezentujący stację drugi szynę. Automat stacji posiada dwa zegary - jeden to liczniki bitów (potrzebny w trakcie wysyłania i odbierania ramek) drugi to zegar który wskazuje, która stacja teraz wysyła. Jeden obrót zegara bitów to przesunięcie zegara stacji o 1. Oprócz tego stacja posiada dwa liczniki - licznik błędów i licznik tych przedziałów, w trakcie których nic nie zostało wysłane.
Stacja może być w jednym z trzech trybów: Normal, reSynchronization, Recovery. Oto rysunki przedstawiające stację podzieloną na 3 części:



A to szyna:

Automat stacji posiada kilkanaście stanów, ich znaczenie jest następujące:

Linki

  1. tdma.xml - projekt w UPPAALu