Specyfikacja i symulacja protokołu komunikacyjnego RIP

• Autorzy: Penczak W. , Obuchowski M.
• Języki publikacji: PL

Abstrakty

PL

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ść.

Słowa kluczowe

PL

protokół RIP; weryfikacja protokołu; symulacja; język Estelle

• Wydawca: Wydawnictwo Uniwersytetu Przyrodniczo-Humanistycznego w Siedlcach
• Czasopismo: Studia Informatica : systems and information technology
• Rocznik: 2004
• Tom: Vol. 1(3)
• Strony: 87--98
• Opis fizyczny: Bibliogr. 15 poz., rys., tab.

Twórcy

autor

Penczak W.

• Akademia Podlaska, Siedlce

autor

Obuchowski M.

• Akademia Podlaska, Siedlce

Bibliografia

• [1] Borzyszkowski A. M. i Srebrny M.: Weryfikacja protokołów kryptograficznych, http://www.signet.pl/archiwum/116.html
• [2] Clarke E., Grunberg O., and Peled D.: Model Checking, The MIT Press, Cambridge, Massachusetts, 1999.
• [3] Dembiński P., Janowska A., Janowski P, Penczek W., Półtora A., Szreter M., Woźna B., Zbrzezny A.: VeriCS: 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] Douglas E. Comer, Dawid L. Stevens. Sieci komputerowe TCP/IP Zasady, protokoły i architektura tom 1, WNT, Warszawa, 1997.
• [5] Douglas E. Comer, Dawid L. Stevens. Sieci komputerowe TCP/IP Projektowanie I realizacja protokołów tom 2, WNT, Warszawa, 1997.
• [6] Institut National des Telecommunications, Estelle Symulator/debugger Edb (v. 4.3) User reference manual, http://www-lor.int-evry.fr/edt/
• [7] Institut National des Telecommunications X Window Interface for EDT (v. 4.3) User reference manual, http://www-lor.int-evry.fr/edt/
• [8] Janowska A.: Intermediate Language for Verics version 1.0, Febraury 2003.
• [9] JPF Web Site, http://ase.arc.nasa.gov/visser/jpf
• [10] Obuchowski M.: Specyfikacja i automatyczna analiza protokołu komunikacyjnego RIP, praca magisterska napisana pod kierownictwem naukowym prof. dr. hab. Wojciecha Penczka, Akademia Podlaska, Siedlce 2003.
• [11] Ratajczak J.: Metody formalne w testowaniu oprogramowania, Software 2.0 11/2002 s. 30-37.
• [12] RFC 1058 Routing Information Protocol
• [13] SLAM Web Site, http://research.microsoft.com/slam/
• [14] VeriCS Web Side, http://www.ipipan.waw.pl/~penczek/verics
• [15] VFSM Web Site, http://cm.bell-labs.com/cm/cs/what/formal_methods/