Reviewing the Service Specification of the IEEE 802.16 MAC Layer Connection Management: A Formal Approach

Abstract

In most of the communication protocol specification documents, there is little, if any, use of more formal techniques for specifying the protocols, such as state and service primitive tables. Thus, these documents are sometimes ambiguous, difficult to understand, and imprecise. The IEEE 802.16 standard document is responsible for specifying and describing the air interface of the BWA systems (Broadband Wireless Access Systems) point to multipoint fixed and mobile networks, and is limited to the description of the MAC(Medium Access Control) layer and physical (PHY). Since the MAC layer is connection-oriented, the standard defines how the connection management service is provided. The service is specified as the occurrence of a set of well-defined service primitives. However, the description of the service specification is somehow informal and presents some ambiguities and inconsistences. So in this paper, we describe the omissions, uncertainties and discrepancies found in the standard documents and propose some solutions to fix these problems. We also provide a formal description of the connection management service specification using Finite State Automata (FSA).