Verifikacija komunikacijskih protokolov na osnovi barvnih Petrijevih mrež

Dolenc, Matej (author), Mraz, Miha (mentor)

V diplomskem delu prikažemo različne metode verificiranja komunikacijskih protokolov. Vsaka izmed metod je na kratko predstavljena, dodatno pa predstavimo še nekaj programskih orodij, ki omenjene metode podpirajo. V nadaljevanju se predvsem osredotočimo na metodo barvnih Petrijevih mrež, ki je grafično orientiran jezik za specifikacijo, simulacijo in verifikacijo komunikacijskih protokolov S pomočjo barvnih Petrijevih mrež lahko poljuben protokol predstavimo kot mrežo, ki je sestavljena iz pogojev in akcij, le-te pa so med seboj povezane z usmerjenimi povezavami. Sledi tudi pregled nekaterih programskih orodij za delo z barvnimi Petrijevimi mrežami, še posebej pa vzamemo pod drobnogled programsko orodje CPN Tools. CPN Tools uporabimo za postavitev modela vedra z žetoni, ki predstavlja protokol, ki se uporablja pri oblikovanju prometa po omrežju. Ko imamo model postavljen, nad njim opravimo postopek verifikacije, v katerem preverimo nekaj najbolj pomembnih lastnosti protokola. Na podlagi pridobljenih rezultatov lahko nato model protokola popravimo in dodatno nadgradimo.

• Language: Slovenian
• Keywords: verifikacija, barvne Petrijeve mreže, CPN Tools
• Work type: Bachelor thesis/paper
• Organization: FRI - Faculty of Computer and Information Science
• Year: 2015
• PID: 20.500.12556/RUL-72139
• Publication date in RUL: 07.09.2015

Secondary language

• Language: English
• Title: Verification of communication protocols with coloured Petri nets

Abstract

In this thesis we point out different methods for verification of communication protocols. Each method is presented in short. In addition, several tools which support mentioned methods are also presented. Next, we primarily focus on a method called coloured Petri nets which is graphically oriented language for specification, simulation and verification of communication protocols. With the help of coloured Petri nets we can present a protocol as a net which consists of places and transitions. Places and transitions are then connected with directional arcs. Then, we take a look at a few tools for work with coloured Petri nets. We mainly focus on a tools called CPN Tools. CPN Tools is used for constructing a model of a token bucket which is a traffic shaping protocol. When the model is constructed we can verify it. During verification we check some of the most important properties of a model. On the basis of results we get, we can then upgrade and fix the erros in the model.

• Keywords: verification, coloured Petri nets, CPN Tools