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

Abstract

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.

Keywords

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

Data

Language: Slovenian
Year of publishing:
Typology: 2.11 - Undergraduate Thesis
Organization: UM FERI - Faculty of Electrical Engineering and Computer Science
Publisher: T. Lavrečnič
UDC: 621.39:004.414.23(043.2)
COBISS: 20022550 Link will open in a new window
Views: 931
Downloads: 72
Average score: 0 (0 votes)
Metadata: JSON JSON-RDF JSON-LD TURTLE N-TRIPLES XML RDFA MICRODATA DC-XML DC-RDF RDF

Other data

Secondary language: English
Secondary title: PROBABILISTIC VERIFICATION OF A CSMA/CA PROTOCOL BY USING PRISM
Secondary abstract: 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.
Secondary keywords: medium access control;wireless personal-area network;formal methods;probablistic timed automation;probabilistic model checking;
URN: URN:SI:UM:
Type (COBISS): Undergraduate thesis
Thesis comment: Univ. v Mariboru, Fak. za elektrotehniko, računalništvo in informatiko, Telekomunikacije
Pages: XIII, 64 str.
ID: 9162549