Specification, verification and simulation of a wireless LAN protocol: MACAW

A formal specification and verification of a wireless LAN protocol is given, and a simulation of the protocol´s performance is also described. The verification is a partial verification in that it does not include a general verification of all possible configurations of the protocol; however, it does cover the expected usage of the protocol, which is for a small number of users sharing a cell. The simulation provides further insight into the protocol, especially concerning its performance. Based on the verification and simulation, some suggestions are made which can improve the protocol´s performance