20.500.12556/DKUM-62430 VERJETNOSTNA VERIFIKACIJA PROTOKOLA CSMA/CA Z ORODJEM PRISM PROBABILISTIC VERIFICATION OF A CSMA/CA PROTOCOL BY USING PRISM 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. 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. krmiljenje dostopa do prenosnega sredstva brezžično osebno omrežje formalne metode verjetnostni časovni avtomat verjetnostno preverjanje modelov medium access control wireless personal-area network formal methods probabilistic timed automaton probabilistic model checking true true false T. Lavrečnič Slovenski jezik Angleški jezik Diplomsko delo 2016-08-26 16:55:08 2016-09-21 14:52:56 2022-06-29 03:08:22 2019-07-11 12:55:19 2016 0 [Maribor 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 621.39:004.414.23(043.2) 20022550 URN:SI:UM:DK:YEN88TWX UN_Lavrencic_Tine_2016.pdf UN_Lavrencic_Tine_2016.pdf 1 B5A0C6308539BA17EBB46116C01C42AA 6be3283f902c5a7c619003a283e102a413bbcc23bd8e1a32be059af04ecdc8a6 2d69074b-7c0d-11eb-bb7a-00155d0001ca https://dk.um.si/Dokument.php?lang=slv&id=100805 Fakulteta za elektrotehniko, računalništvo in informatiko 0 0 0