diplomsko delo
Tine Lavrenčič (Avtor), Tatjana Kapus (Mentor)

Povzetek

V diplomskem delu je predstavljena verjetnostna verifikacija protokola CSMA/CA iz standarda IEEE 802.15.4 za brezžična osebna omrežja z orodjem PRISM. Po kratki predstavitvi standarda 802.15.4 in opisu njegovih protokolov za dostop do prenosnega sredstva smo se osredotočili le na omrežje z dvema oddajnima postajama z nerežnim protokolom CSMA/CA in ga najprej predstavili s časovnimi avtomati v orodju UPPAAL. Iz modela s časovnimi avtomati smo nato tvorili formalno specifikacijo v obliki verjetnostnih časovnih avtomatov za orodje PRISM. Z orodjem PRISM smo verificirali nekatere verjetnostne lastnosti, ki naj bi jih protokol CSMA/CA po standardu 802.15.4 imel. Pri tem smo verificirali tudi eno izmed izboljšav protokola, predlagano v literaturi.

Ključne besede

krmiljenje dostopa;brezžično osebno omrežje;formalne metode;verjetnostni časovni avtomat;verjetnostno preverjanje modelov;diplomske naloge;

Podatki

Jezik: Slovenski jezik
Leto izida:
Tipologija: 2.11 - Diplomsko delo
Organizacija: UM FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
Založnik: T. Lavrečnič
UDK: 621.39:004.414.23(043.2)
COBISS: 20022550 Povezava se bo odprla v novem oknu
Št. ogledov: 931
Št. prenosov: 72
Ocena: 0 (0 glasov)
Metapodatki: JSON JSON-RDF JSON-LD TURTLE N-TRIPLES XML RDFA MICRODATA DC-XML DC-RDF RDF

Ostali podatki

Sekundarni jezik: Angleški jezik
Sekundarni naslov: PROBABILISTIC VERIFICATION OF A CSMA/CA PROTOCOL BY USING PRISM
Sekundarni povzetek: This diploma thesis presents the probabilistic verification of a CSMA/CA protocol of IEEE 802.15.4 standard for wireless personal-area networks by using PRISM. It begins with a short presentation of IEEE 802.15.4 standard and the description of its protocol for medium access. Afterwards, we focused only on the network with two unslotted CSMA/CA transmitting stations, firstly being presented with timed automata in UPPAAL. From the timed automata model we made a formal specification in a form of probabilistic timed automata in PRISM. Using PRISM, we verified some probabilistic properties the IEEE 802.15.4 standard CSMA/CA protocol should have. We also verified an improvement of the protocol, which has been proposed in the literature.
Sekundarne ključne besede: medium access control;wireless personal-area network;formal methods;probablistic timed automation;probabilistic model checking;
URN: URN:SI:UM:
Vrsta dela (COBISS): Diplomsko delo
Komentar na gradivo: Univ. v Mariboru, Fak. za elektrotehniko, računalništvo in informatiko, Telekomunikacije
Strani: XIII, 64 str.
ID: 9162549