Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: weryfikacja protokołu

Sortuj według:

Ogranicz wyniki do:

Modelowanie i weryfikacja protokołu SCTP z wykorzystaniem automatów czasowych ze zmiennymi

Męski A., Półrola A.

Zeszyty Naukowe Wyższej Szkoły Informatyki

2008

Vol. 7, Nr 1

49-67

W pracy konstruujemy model protokołu SCTP (Stream Transmission Control Protocol) - protokołu transportowego zawierającego szereg mechanizmów mających zapewnić niezawodne dostarczanie. Do modelowania protokołu używamy automatów czasowych ze zmiennymi całkowitymi. Otrzymany model wykorzystywany jest następnie do automatycznej weryfikacji protokołu, podczas której testujemy własności wyrażone za pomocą formuł logiki temporalnej CTL (ang. Computation Tree Logic).

In the paper we construct a model for SCTP (Stream Control Transmission Protocol) - a transport layer protocol which provides mechanisms of reliable delivery. The protocol is modelled by a set of timed automata augmented with integer variables. The resulting model is then used to test the protocol w.r.t. certain properties expressed by the formulas of the temporal logic CTL (Computation Tree Logic).

Specyfikacja i symulacja protokołu komunikacyjnego RIP

Penczak W., Obuchowski M.

Studia Informatica : systems and information technology

2004

Vol. 1(3)

87--98

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