Title :
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
fDate :
6/1/1990 12:00:00 AM
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;
Journal_Title :
Control Systems Magazine, IEEE
