VERJETNOSTNA VERIFIKACIJA PROTOKOLA CSMA/CA Z ORODJEM PRISMLavrenčič, Tine (Avtor) Kapus, Tatjana (Mentor) krmiljenje dostopa do prenosnega sredstvabrezžično osebno omrežjeformalne metodeverjetnostni časovni avtomatverjetnostno preverjanje modelovV 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.T. Lavrečnič20162016-08-26 16:55:08Diplomsko delo62430UDK: 621.39:004.414.23(043.2)COBISS_ID: 20022550NUK URN: URN:SI:UM:DK:YEN88TWXsl