Improving the specification of the WiMax ARQ operation

WiMax, includes a rich set of MAC layer features. The use of retransmission algorithms for supporting reliable delivery in the presence of errors is optional, so the standard defines two types of connections: Automatic Repeat Request (ARQ)-enabled connections and non-ARQ connections. A SDU (Service data Unit) is logically partitioned into ARQ blocks, which represent the basic units of transmission and retransmission. As a complex system, the need for a clear and unambiguous specification is very important. Thus, we have studied the ARQ operation as defined in the specification for protocol verification. We have found several issues in specification of the ARQ operation. We describe the problems found in the specification and propose some solutions. So, we use Colored Petri Nets (CPNs) to model the improved specification of the ARQ operation. Then, the CPN model is analyzed for correct behavior. Finally we present a new ARQ transmit block state machine.