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

Author

Brooks, Charles A. ; Cieslak, Randy ; Varaiya, Pravin

Author_Institution

Dept. of Electr. Eng. & Comput. Sci., California Univ., Berkeley, CA, USA

Volume

10

Issue

4

fYear

1990

fDate

6/1/1990 12:00:00 AM

Firstpage

87

Lastpage

94

Abstract

A successful approach to problems of protocol specification, implementation, and verification is presented. Protocols are specified in a language called LIFP (Language for Implementing Fast Protocols) which is based on a model of interacting state machines. A compiler translates LIFP specifications into code that can be executed on PNPS (programmable network prototyping system), an experimental network emulator developed at the University of California at Berkeley. Verification of a LIFP control 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.<>

Keywords

computer networks; program compilers; program debugging; protocols; LIFP; compiler; debugger; discrete event system; implementation; media access control protocols; network emulator; network environment; programmable network prototyping systems; specification; state machines; supervisory control; verification; Access protocols; Communication networks; Discrete event systems; Ethernet networks; Feedback; Hardware; Local area networks; Media Access Protocol; Supervisory control; Token networks;

fLanguage

English

Journal_Title

Control Systems Magazine, IEEE

Publisher

ieee

ISSN

0272-1708

Type

jour

DOI

10.1109/37.56282

Filename

56282