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. Kwiatkowska and G. Norman and J. Sproston
Probabilistic Model Checking of the {IEEE} 802.11 Wireless Local Area Network Protocol
Proc. 2nd Joint International Workshop on Process Algebra and Probabilistic Methods,
Performance Modeling and Verification (PAPM/PROBMIV'02)}, volume 2399 of LNCS,
pages 169-187, Springer, 2002.

[KNPS06]
M. Kwiatkowska, G. Norman, D. Parker and J. Sproston
Performance Analysis of Probabilistic Timed Automata using Digital Clocks
Formal Methods in System Design, 29:33-78, 2006