Analysis and Design of Communication Protocols

Przedmiot dotyczy jednego z podstawowych zagadnień w dziedzinie telekomunikacji, jakim jest projektowanie, implementacja i weryfikowanie protokołów komunikacyjnych. W odróżnieniu od innych dziedzin (jak np. teoria kolejek), w których nacisk został położony na zjawiska o charakterze ilościowym - stochastycznym, przedmiot niniejszy koncentruje się na poprawności logicznej i metodach jej uzyskania zarówno w teorii, jak i w praktyce telekomunikacyjnej. Jako podstawę dla rozważań wprowadza się specyficzny aparat formalny, pokrewny teorii grafów / automatów / procesów.

Przedmiot dotyczy jednego z podstawowych zagadnień w dziedzinie telekomunikacji, jakim jest projektowanie, implementacja i weryfikowanie protokołów komunikacyjnych. W odróżnieniu od innych dziedzin (jak np. teoria kolejek), w których nacisk został położony na
zjawiska o charakterze ilościowym - stochastycznym, przedmiot niniejszy koncentruje się na poprawności logicznej i metodach jej uzyskania zarówno w teorii, jak i w praktyce telekomunikacyjnej. Jako podstawę dla rozważań wprowadza się specyficzny aparat formalny, pokrewny teorii grafów / automatów / procesów.



Treść wykładu
Wprowadzenie. Charakterystyka systemów telekomunikacyjnych jako dużych, rozproszonych systemów czasu rzeczywistego. Pojęcie protokołu (Merlin). Rola i miejsce dziedziny protocol science. Historia badań nad protokołami (2h).

Protokół jako abstrakcja systemu. Podstawowe zagadnienia projektowania systemu. Własności protokołu: generyczne (reguły poprawnej konstrukcji) i specyficzne. Bezpieczeństwo / żywotność. Konstruktywne i korektywne podejście do cyklu życiowego. Weryfikacja i walidacja (2h).

Specyfikacja a opis. Cele i aspekty formalizacji. Języki i formalizmy: SDL, Estelle, Lotos, MSC, ASN.1+BER, TTCN. Baza semantyczna dla opisu cech behawioralnych protokołu: logiki temporalne, algebry procesów, model automatowy (2h).

Szczegółowa dyskusja modelu automatowego. Automat globalny a automaty poszczególnych procesów. Style specyfikacji. Formalizacja: FSM, EFSM. Konwencja notacyjna Zafiropulo. Model systemu: CEFSM. Modele kanałów komunikacyjnych. Stan globalny syntaktyczny a osiągalny. Zachowanie systemu: przeplot zdarzeń, ślad. Przestrzeń stanów osiągalnych. Modele błędów jako predykaty na stanach osiągalnych (4h).

Konstruowanie grafu osiągalności: wszerz, wgłąb. Jakość i pokrycie
metod eksploracji przestrzeni stanów. Eksploracja pełna i cząstkowa. Zapis informacji o stanie z kompresją - metoda Holzmanna (supertrace, bitstate hashing). Wielokrotna eksploracja z kompresją (multihash): równoległa i szeregowa. Heurystyki zwiększania jakości eksploracji. Metoda analizy osiągalności zredukowanej (Cacciari). Eksploracja bez zapisu informacji o stanie (random walk) (4h).

Język MSC (Message Sequence Chart). Całkowity i częściowy porządek zdarzeń. Elementy języka. Spójność zachowania systemu z wyspecyfikowanym porządkiem częściowym. Zastosowanie do weryfikacji cech nie dających się przedstawić jako predykaty na stanach osiągalnych (3h).

Protokół w funkcjonalnej architekturze warstwowej: model i uwarunkowania implementacyjne. Struktura elementów statycznych protokołu: definicja tabelaryczna, język ASN.1 / reguły kodowania BER (3h).

Weryfikacja implementacji - pojęcia podstawowe: testowanie bierne i czynne; testowanie zgodności i zdolności do współpracy. Model testowania zgodności oparty na relacjach implementowania (imp) i relacjach spełnienia (sat). Przemysłowe testowanie zgodności w telekomunikacji - norma ISO 9646. Cechy protokołu w normach - formularze PICS. Zgodność statyczna i dynamiczna. Istota i technika formułowania wymagań względem implementacji (2h).

Szczegółowa dyskusja testowania zgodności: system testujący / testowany, architektury testowe, metody i kontekst testowania, cel i struktura testu, struktura i pokrycie zestawu testów. Język TTCN2 - konstrukcje, semantyka i przykłady użycia. Informacja o języku TTCN3. Standaryzowany proces oceny zgodności (4h).

Metody automatycznego generowania testów zgodności ze specyfikacji w postaci automatu FSM: DS, W, E, UIO. Inne rodzaje testów. Teoria i zastosowania testowania biernego (2h).

Struktura norm telekomunikacyjnych dla protokołów. Podsumowanie (2h).



Zakres projektu
W ramach projektu studenci rozwiązują, w niewielkich grupach, problemy projektowe bądź analityczne wskazane przez prowadzącego. Przykłady projektów: zaprojektować i zaimplementować system automatycznej weryfikacji protokołów zadanych w postaci sieci automatów FSM; wyspecyfikować jako protokół i przy użyciu poznanych metod zbadać zachowanie znanego z literatury generycznego problemu (np. wybór monitora w sieci pierścieniowej, problem jedzących filozofów); zaprojektować i zaimplementować model systemu wykrywającego zadane wzorce zachowań w systemie rzeczywistym.

1. G.J.Holzmann, Design and Validation of Computer Protocols. Prentice Hall, 1991
2. 
   K.M.Brzeziński,Wprowadzene do testowania protokołów telekomunikacyjnych. Skrypt, CITCOM-PW
3. wskazane i udostępnione przez prowadzącego standardy telekomunikacyjne i artykuły m.in. z konferencji FORTE, PSTV, Testcom.