Specyfikacja i automatyczna analiza protokołu komunikacyjnego

• Autorzy: Teodorczuk P. , Penczek W.
• Języki publikacji: PL

Abstrakty

PL

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.

Słowa kluczowe

PL

protokół TCP; modelowanie protokołu TCP; analiza protokołu TCP; specyfikacja; język Estelle

• Wydawca: Wydawnictwo Uniwersytetu Przyrodniczo-Humanistycznego w Siedlcach
• Czasopismo: Studia Informatica : systems and information technology
• Rocznik: 2003
• Tom: Vol. 2(2)
• Strony: 49--59
• Opis fizyczny: Bibliogr. 9 poz., rys., tab.

Twórcy

autor

Teodorczuk P.

• Akademia Podlaska, Siedlce

autor

Penczek W.

• Akademia Podlaska, Siedlce

Bibliografia

• [1] R. Braden, Requirements for Internet Hosts-Communication Layers, RCF-1122, October 1989.
• [2] E. Clark, O. Gurnberg, D. Peled, Model Checking, The MIT Press, Cam- bridge, Massachusetts, 1999.
• [3] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półtora, M. Szreter, B. Woźna, and A. Zbrzezny. VerlCS: A tool for verifying Timed Automata and Estelle specifications. In Proc. Of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’03), volume 2619 of LNCS, pages 278-283. Springer-Verlag, 2003.
• [4] KRONOS Web Side, http://www-verimag.imag.fr/TEMPORISE/kronos/
• [5] W. Penczek, B. Woźna, and A. Zbrzezny. SAT-based bounded model checking for the universal fragment of TCTL. Technical Report 947, ICS PAS, Ordona 21, 01-237 Warsaw, August 2002.
• [6] W. Penczek, B. Woźna, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. Of the 7th Int. Symp. On Formal Techniques in Real-Time and Fault Tolerant System (FTRTFT’02), volume 2469 of LNCS, pages 265-288. Springer-Verlag, 2002.
• [7] J. Postel, Transmission Control Protocol, RCF-793, September 1981.
• [8] P. Teodorczuk, Specyfikacja i automatyczna analiza protokołu komunikacyjnego TCP, praca magisterska, Akademia Podlaska, Siedlce, 2003.
• [9] VeriCS Web Side, http://www.ipipan.waw.pl/~penczek/verics