Formal Specification and Analysis of a Wireless Media Access Protocol.

reportActive / Technical Report | Accession Number: ADA304483 | Open PDF

Abstract:

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.

Author(s):
Almquist, Martin S.
Author Organization(s):
NAVAL POSTGRADUATE SCHOOL MONTEREY CA
Descriptive Note:
Master's thesis,
Pagination:
0096

Security Markings

DOCUMENT & CONTEXTUAL SUMMARY

Distribution:
Approved For Public Release

RECORD

Collection: TR
Identifying Numbers
Monitor Series:
NPS
 Subject Terms
Joint Capability Areas:
JCA_6.1.2_Wireless Transmission; JCA_6.1_Information Transport; JCA_6_Net Centric; JCA_5.3_Planning; JCA_5_Command and Control
Communities of Interest:
No COI(s) Identified
Descriptor(s):
*SPECIFICATIONS, *COMMUNICATIONS NETWORKS, *SYSTEMS APPROACH, *DIGITAL COMMUNICATIONS, INFORMATION EXCHANGE, MODELS, THESES, MILITARY APPLICATIONS, ACCESS, MEDIA, TRANSITIONS, SYSTEMS ANALYSIS, MESSAGE PROCESSING
Field(s)/Group(s):
Radio Communications
Keyword(s):
*WIRELESS MEDIA, *PROTOCOLS, MACAW(MULTIPLE ACCESS COLLISION AVOIDANCE WIRELESS), MAC(MEDIA ACCESS CONTROL), PACKET RADIO NETWORKS
Report Date:
1995 Sep 01