s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
3593 Commits
5 Branches
0 Tags
31 MiB
 
 
 
 
 
 
Branch: master
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'master'
${ noResults }
prism-accumulation/prism-examples/wlan
Dave Parker a00471be4b
Added txt extension to README files. 		15 years ago
..
README.txt Added txt extension to README files. 15 years ago
auto Tweaked some auto files. 17 years ago
wlan.pctl added wlan example to examples 17 years ago
wlan0.nm added wlan example to examples 17 years ago
wlan0_collide.nm added wlan example to examples 17 years ago
wlan0_time_bounded.nm added wlan example to examples 17 years ago
wlan1.nm added wlan example to examples 17 years ago
wlan1_collide.nm added wlan example to examples 17 years ago
wlan1_time_bounded.nm added wlan example to examples 17 years ago
wlan2.nm added wlan example to examples 17 years ago
wlan2_collide.nm added wlan example to examples 17 years ago
wlan2_time_bounded.nm added wlan example to examples 17 years ago
wlan3.nm added wlan example to examples 17 years ago
wlan3_collide.nm added wlan example to examples 17 years ago
wlan3_time_bounded.nm added wlan example to examples 17 years ago
wlan4.nm added wlan example to examples 17 years ago
wlan4_collide.nm added wlan example to examples 17 years ago
wlan4_time_bounded.nm added wlan example to examples 17 years ago
wlan5.nm added wlan example to examples 17 years ago
wlan5_collide.nm added wlan example to examples 17 years ago
wlan5_time_bounded.nm added wlan example to examples 17 years ago
wlan6.nm added wlan example to examples 17 years ago
wlan6_collide.nm added wlan example to examples 17 years ago
wlan6_time_bounded.nm added wlan example to examples 17 years ago
wlan_collide.pctl added wlan example to examples 17 years ago
wlan_time_bounded.pctl added wlan example to examples 17 years ago

README.txt 

This case study concerns the IEEE 802.11 Wireless LAN

We consider the scenario where two stations trying to send packets simultaneously.

The PRISM model is taken from [KNS02a] using the integer semantics given in [KNS06]. In the model one time unit
corresponds to 50μs and to ensure integer bounds, where neccessary, scaling lower bound constraints down and
upper bound constraints up to sensure a sound abstraction.


For more information on the probabilistic timed automata see: http://www.prismmodelchecker.org/casestudies/wlan.php

PARAMETERS

wlanK.nm - K is the maximum value of a stations backoff counter where 6 is specified in the standard
TRANS_TIME_MAX - maximum time to send a packet where (after scaling) 315 specified in the standard
COL=2: in collosion model to count number collisions (parameter k in the property files must be less than or equal to COL)
DEADLINE: in time_bounded model is the deadline

=====================================================================================

[KNS02a]
M. Kw