Modelling medium access control in IEEE 802.15.4 nonbeacon-enabled networks with probabilistic timed automata

Povzetek

This paper concerns the formal modelling of medium access control in nonbeacon-enabled IEEE 802.15.4 wireless personal area networks with probabilistic timed automata supported by the PRISM probabilistic model checker. In these networks, the devices contend for the medium by executing anunslotted carrier sense multiple access with collision avoidance algorithm. In the literature, a model of a network which consists of two stations sendingdata to two different destination stations is introduced. We have improved this model and, based on it, we propose two ways of modelling a network with an arbitrary number of sending stations, each having its own destination. We show that the same models are valid representations of a starshaped network with an arbitrary number of stations which send data to thesame destination station. We also propose how to model such a network if some of the sending stations are not within radio range of the others, i.e. ifthey are hidden. We present some results obtained for these models by probabilistic model checking using PRISM.

Ključne besede

wireles personnal area network;medium access control;hidden station;formal specification;probabilistic model checking;

Podatki

Jezik:	Angleški jezik
Leto izida:	2013
Tipologija:	1.01 - Izvirni znanstveni članek
Organizacija:	UM FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
UDK:	659.2
COBISS:	16807958
ISSN:	1574-017X
Matična publikacija:	Journal of mobile information systems
Št. ogledov:	760
Št. prenosov:	311
Ocena:	0 (0 glasov)
Metapodatki:

Ostali podatki

Sekundarni jezik:	Slovenski jezik
Sekundarne ključne besede:	osebno brezžično omrežje;krmiljenje dostopa do medija;skriti terminal;formalna specifikacija;verjetnostno preverjanje modelov;
URN:	URN:SI:UM:
Vrsta dela (COBISS):	Znanstveno delo
Strani:	str. 157-188
Letnik:	ǂVol. ǂ9
Zvezek:	ǂno. ǂ2
Čas izdaje:	2013
DOI:	10.3233/MIS-130160
ID:	10842823