Specyfikacja i automatyczna analiza protokołu komunikacyjnego

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.