Title: Quantitative Verification of WiMAX Traffic Shaping Solutions
Abstract: The IEEE 802.16 (WiMAX) standard defines a set of QoS sensitive mechanisms for regulating the access to Broadband Wireless networks. In this paper we present a formal quantitative verification study of different Traffic Shaping (TS) solutions as proposed in the literature. In particular we consider a priority-based TS (TS-pri) and a probability-based TS (TS-prob) and we compare them by means of probabilistic model checking verification. In this way the performance tradeoffs between strictness (i.e. TS-pri) and fairness (i.e. TS-prob) can be formally quantified and the desired configuration of the TS mechanism can be chosen accordingly.