WPROWADZENIE

Opisywana praca powstała w roku 1996 w wyniku współpracy grupy z Aalborg University (Klaus Havelund, Arne Skou, Kim Guldstrand Larsen, Kristian Lund) a duńską firmą Bang & Olufsen. Jest przykładem zastosowania UPPAALa do rozwiązania typowo przemysłowego problemu.

Analizie poddany został protokół komunikacyjny dla urządzeń audio/video firmy B&O. Protokół zawierał nieznany błąd, który objawiał się okazjonalnym gubieniem danych.

Stworzenie modelu zostało przeprowadzone w 5 iteracjach i zajęło 3 miesiące. Dokumentacja protokołu składała się wyłącznie z diagramów przepływu (flow charts; 3 strony) i kodu w assemblerze (2800 linii). Model tworzono w oparciu głównie o symulację, analizę diagramów i rozmowy z B&O. Kilkukrotnie pojawiła się potrzeba wyciągania szczegółów z kodu. Ostateczna wersja została zaakceptowana przez B&O jako prawidłowa abstrakcja istniejącej implementacji.

Graficzna reprezentacja automatów z czasem okazała się bardzo dobrym sposobem komunikacji pomiędzy twórcami protokołu a grupą zajmującą się weryfikacją.

   PROTOKÓŁ

  Środowisko

Środowisko, w którym protokół działa, to magistrala (bus) i podłączone do niej urządzenia audio/video.

  Niższe warstwy protokołu

Magistrala przyjmuje dwa stany: 0 i 1. Działa przy tym na zasadzie koniunkcji - jeśli jakiekolwiek urządzenie nadaje 0, to magistrala jest w stanie 0. Z tego powodu cisza reprezentowana jest przez 1.

Podstawową jednostką przesyłaną przez magistralę jest ramka. Ramka zbudowana jest z T-messages w następujący sposób:

T₅ ( T₁ | T₂ | T₃ )^>14 T₄

T-message T_i ma następującą postać.

Wprowadza się też pojęcie sygnału zakłócającego (jamming signal), który jest reprezentowany przez 0 nadawane przez 25 ms. Jest on nadawany przez urządzenie, które wykryje kolizję.

  Wyższe warstwy protokołu

Protokół został podzielony na 4 fazy:

1. Faza bezczynności (idle)
2. Faza inicjalizacji (initialization)
3. Faza transmisji (transmission)
4. Faza obsługi kolizji (collision handling phase)

Wyspecyfikowano też szereg reguł, opisujących zachowanie protokołu.

• Bus Reservation Rule
  Nadanie T₅ rezerwuje magistralę dla procesu, który go nadał, a nadanie T₄ zwalnia.
• Frame Gap Rule
  Pomiędzy ramkami wymagana jest przerwa 50 ms.
• Frame Initialization Rule
  Faza inicjalizacji trwa dwa okresy, podczas którego urządzenie sprawdza, czy na magistrali jest 1 (cisza).
• Bus Sample Rule
  W fazie transmisji urządzenie musi spawdzać co pół okresu jaki jest stan magistrali - na początku okresu i w jego połowie.
• Bus Output Rule
  Mówi o opóźnieniu w zmianie stanu magistrali (ograniczenie fizyczne).
• Collision Detection Rule
  Kolizję wykrywa się porównując rzeczywisty stan magistrali ze stanem oczekiwanym.
• Collision Handling Rule
  Opisuje jak reagować na wykrytą kolizję - kiedy nadawać sygnał zakłócający, a kiedy wrócić do fazy inicjalizacji i czekać aż inne urządzenie skończy zakłócanie.
• Transmission Stop Rule
  Po wykryciu kolizji transmisja jest przerywana.
• Detection Stop Rule
  Mówi kiedy należy zakończyć sprawdzanie stanu magistrali (po dwóch okresach kończącego ramkę T₄).
• Protocol Correctness
  
  • Jeśli ramka nadawana przez urządzenie zostanie zniszczona, to wykryje ono to.
  • Jeśli jakieś urządzenie wykryje kolizję, to wykryją ją wszystkie nadające urządzenia.

   MODEL

Przy tworzeniu modelu pominięto nieistotne aspekty protokółu i implementacji - dla przykładu nie jest w żaden sposób modelowane odbieranie ramek.

Ostateczna wersja modelu składa się z 9 automatów:

Komunikacja odbywa się przez kanału i zmienne dzielone. Każde urządzenie posiada jeden zegar lokalny, który znajduje się w Sender.

  Bus

  Frame_Generator_A

  Detector_A

  Sender_A

   WERYFIKACJA

Sformułowanie reguły poprawności nie było proste, bowiem należało to zrobić tak, aby wykryć błąd, o którego źródle nic nie było wiadomo. Podobnie jak model reguła poprawności przeszła przez kilka iteracji.

Przypomnijmy:

• Jeśli ramka nadawana przez urządzenie zostanie zniszczona, to wykryje ono to.
• Jeśli jakieś urządzenie wykryje kolizję, to wykryją ją wszystkie nadające urządzenia.

Trzeba zdefiniować co oznacza, że ramka została zniszczona. Ramkę uznajemy za zniszczoną, jeśli bity nadawane przez urządzenie są różne od wartości odczytanych przez urządzenie z magistrali.

Automat Observer jest wprowadzony do systemu po to, aby sprawdzać poprawność.

  Observer_A

Forumuła odpowiedzialna za poprawność wyraża się następująco:

A[] (A_eof == 1 imply (A_diff == 0 and B_res == 0))

W celu wydajnej weryfikacji z opisanego modelu wyprowadzoną prostszą wersję. Automat Frame_Generator zmodyfikowano tak, aby produkował ramki zawierające wyłącznie T₁. Rozważano także dwa inne ograniczenia:

• urządzenie wysyła tylko jedną ramkę,
• oraz ograniczenie liczby T-messages w jednej ramce.

  Błąd

UPPAAL wykrył, że tak sforumłowana reguła poprawności nie jest spełniona. W uproszczonej wersji modelu zajęło mu to kilka minut. Ślad składał się z 1998 pojedynczych tranzycji. Można zatem spodziewać się, że znalezienie tego błędu bez pomocy narzędzia byłoby bardzo trudne.

Ślad, który wygenerował UPPAAL można, nie wchodząc w szegóły opisać następująco:

Urządzenie A wysyła ramkę składającą się z 15 T₁. Urządzenie B wysyłą ramkę składającą się z 16 T₁. Ramki są identyczne aż do T₄ kończącej ramkę wysłaną przez A. Dodatkowo B wysyła swoją ramkę z opóźnieniem dokładnie 40 * 10^-6s w stosunku do A.
Okazuje się, że B wykryje kolizję i zacznie zakłocać. Natomiast A kończy wykrywanie kolizji zbyt szybko, by to zauważyć - ramka wysłana przez A jest zniszczona i nie będzie zretransmitowana.

Warto wspomnieć o tym, że gdy znana była przyczyna błędu, udało się wywołać go "w rzeczywistości" (w laboratorium B&O).

   POPRAWIONY MODEL

Wina leży w Detection Stop Rule. Regułę tę wprowadzno, aby zapobiec duplikacji ramek, które pojawiło by się, gdyby wykrywanie kolizji było przeprowadzane zbyt długo. Rozwiązanie problemu było proste - należy zakończyć wykrywanie kolizji troszeczkę później (nie wchodząć w szczegóły).

Po wprowadzeniu stosownych modyfikacji do modelu okazało się, że UPPAAL zweryfikował regułę poprawności pozytywnie. Zajęło mu to na uproszonej wersji modelu około 30 minut.

   PODSUMOWANIE

W wyniku zastosowania UPPAALa udało się znaleźć błąd w istniejącym i używanym protokole "przemysłowym". Co więcej, wydaje się, że znalezienie tego błędu tradycyjnymi metodami byłoby trudne.

UPPAAL pomógł też w zweryfikowaniu poprawności nowej wersji algorytmu.

Warto podkreślić jeszcze raz, że graficzna reprezentacja automatów z czasem okazała się bardzo skutecznym sposobem komunikacji.

_{Pliki UPPAALowe znajdują się tutaj.}