Modeling and Functional Validation of the IEEE 802.16 MAC Protocol for the Management of Connections and Dynamic Service Flows

The IEEE 802.16 standard specifies and describes the air interface of the Broad-band Wireless Access Systems point to multipoint fixed and mobile networks, and it is limited to the description of the MAC (Medium Access Control) layer and physical (PHY) layer. The standard defines informally an unmanageable set of procedures associated with the service flows (SF) at the MAC layer, also related to a connection element called dynamic service flows (DSF). This research defines the management of these connections as “IEEE 802.16 MAC Protocol for Connection Management and DSF”, and studies the protocol to facilitate the re-use of some of concepts in the specification of emerging wireless networks. This research modeled and analyzed the protocol using Colored Petri Nets and the protocol verification methodology proposed by J. Billington. The results are a de-tailed and precise description of the protocol, and the service specification; the functional validation of such models through the determination of regular expressions of the language; the generation of the protocol language and the service specification; different drawbacks in the specification; and the PROSEGA/CPN Software to simplify the analysis of the models.