Formal modeling and analysis of greedy behaviors in IEEE 802.11 protocols

In this paper we present a formal modeling and analysis approach of the IEEE 802.11 CSMA/CA protocol in wireless local area networks (LANs) whose some greedy stations have selfish behaviors. Such stations do not strictly comply with rules of CSMA/CA protocol in order to increase their chances to access the channel at the expense of normal stations. We capture the behavior of wireless stations correctly implementing the DCF functioning mode of CSMA, along with compromised stations and the wireless medium using communicating timed automata which are the modeling language of the UPPAAL model checker. We proceed as well to the checking of some safety and liveness properties by means of this tool. We also propose stochastic models and we give some numerical results.