Formal specification and analysis of a wireless media access protocol
Download
Author
Almquist, Martin Scott
Date
1995-09Advisor
Lundy, Gilbert M.
Metadata
Show full item recordAbstract
The problem addressed by this research is to formally specify and analyze a proposed wireless network media access protocol. The protocol, named MACAW for Multiple Access Collision Avoidance Wireless, was described in ACM SIGCOMM Proceedings 94 Vol. 24 #4. The approach taken was to use the formal model Systems of Communicating Machines to develop a formal specification of the protocol. An initial specification was derived directly from the original proposal in order to reveal any unresolved problems. The formal specification was then refined to produce a more precise and unambiguous specification. The refined specification was used to analyze the protocol using system state analysis for properties such as liveness and deadlock. Liveness is the property of positive progression while deadlock is an undesirable property where a state is reached that cannot be left. The results are a specification of MACAW as originally proposed and a refined specification which provides an unambiguous understanding of the protocol. The analysis determined that the protocol is free of deadlock. Also presented are three new transitions between MACAW states, which were suggested by the analysis.
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.Collections
Related items
Showing items related by title, author, creator and subject.
-
Specification and analysis of a high speed transport protocol
Tipici, H. Alphan. (Monterey, California. Naval Postgraduate School, 1993-06);While networks have been getting faster, perceived throughput at the application has not always increased accordingly and the bottleneck has moved to the communications processing part of the system. The issues that cause ... -
A specification and analysis of the IEEE token bus protocol
Charbonneau, Lauren J. (Monterey, California. Naval Postgraduate School, 1990-06);In this thesis a formal description technique, systems of communicating machines, is used to specify and analyze a token bus protocol. A simplified description of the protocol is given, and proofs of certain correctness ... -
Specification and analysis of the SNR high-speed transport protocol
Lundy, Gilbert M.; Tipici, H. Alphan (IEEE, 1994-10);In recent years the emergence of optical fiber and its correspondingly high data rates have led to the development of much higher speed networks, both locally and over the long haul. These developments led to the design ...