A method for specifying, implementing, and verifying media access control protocols

A media access control (MAC) protocol is a feedback policy that nodes in a communication network must follow to ensure proper access to a shared medium in the network. MAC protocols for common local area networks such as Ethernet and token rings are standardized by national and international committees. This article presents a successful approach to problems of protocol specification, implementation, and verification. Protocols are specified in a language called LIFP which is based on a model of interacting state machines. A compiler translates LIFP specifications into code that can be executed on PNPS, an experimental network emulator developed at the University of California at Berkeley. Verification of a LIFP protocol is facilitated by a debugger that simulates both PNPS hardware and the network environment in which the protocol is supposed to operate. This approach is compared with others (SPANNER and ESTELLE). Some aspects of the problem of protocol design allow it to be usefully viewed as one of supervisory control of a discrete event system. However, other aspects of protocol design show that current theories of supervisory control are inadequate.