W pracy opisano specyfikację (w języku Estelle), a następnie symulację protokołu komunikacyjnego Routing Information Protocol (RIP). Zarówno konstrukcję specyfikacji, jak i jej weryfikację przeprowadzono za pomocą narzędzi Estelle Development Toolset. Wskazano główne kroki w tworzeniu specyfikacji oraz naszkicowano techniki symulacyjne użyte do jej weryfikacji. Symulacja pozwoliła na stwierdzenie braku występowania błędów dynamicznych specyfikacji. Ponadto wykazano podstawowe własności protokołu dla zapewnienia poprawności problemu trasowania w systemach sieci komputerowej, jak brak występowania pętli w trasowaniu, niezawodność oparta na zasadzie „k spośród n”, odporność na awarie bram czy też poprawne działanie algorytmu wektor-odległość.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
W pracy opisano automatyczną walidację protokołu TCP. W tym celu została napisana specyfikacja protokołu TCP w języku Estelle. Następnie przeprowadzono symulację z użyciem pakietu EDT. Część sterująca protokołu TCP została poddana weryfikacji modelowej przy użyciu narzędzi Verics i Kronos. Dla wszystkich testowanych i weryfikowanych własności potwierdzono poprawność protokołu TCP. Mimo iż weryfikacja modelowa pełnego protokołu nie została przeprowadzona, to jego specyfikacja w Estelle będzie podstawą do dalszych prób dokonania takiej weryfikacji.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.