Scalable Probabilistic Models for 802.11 Protocol Verification

TL;DR

This paper enhances probabilistic model checking for the IEEE 802.11 MAC protocol by simplifying models and optimizing them, enabling verification of larger networks with preserved probabilistic properties.

Contribution

It introduces methods to scale probabilistic model checking for 802.11 MAC by model simplification and optimization, expanding applicability to larger network sizes.

Findings

Significant reduction in model complexity achieved.

Verification of larger networks becomes feasible.

Preservation of probabilistic reachability measures.

Abstract

The IEEE 802.11 protocol is a popular standard for wireless local area networks. Its medium access control layer (MAC) is a carrier sense multiple access with collision avoidance (CSMA/CA) design and includes an exponential backoff mechanism that makes it a possible target for probabilistic model checking. In this work, we identify ways to increase the scope of application of probabilistic model checking to the 802.11 MAC. Current techniques do not scale to networks of even moderate size. To work around this problem, we identify properties of the protocol that can be used to simplify the models and make verification feasible. Using these observations, we directly optimize the probabilistic timed automata models while preserving probabilistic reachability measures. We substantiate our claims of significant reduction by our results from using the probabilistic model checker PRISM.