Specification and Analysis of the IEEE (Institute of Electrical and Electronic Engineers) Token Ring Protocol.

摘要

Computer communications are becoming increasingly important in the command, control and communications community. Using models to verify that the communication protocols used by these computers function properly is a time and effort saving device. A model called systems of communicating machines combines two types of models, finite state machines and programming language models. In this thesis systems of communicating machines is used to specify and analyze the IEEE token ring protocol. The specification makes several simplifying assumptions about the protocol in order to make the analysis manageable. These simplifications include limiting the network to two machines and shortening the frame and token formats to reduce the number of transmissions on the network. This thesis exercises the resulting specification to both verify that the protocol won't fail and that the specification is correct. The type of analysis used in this thesis is called a reachability analysis or a system state analysis. This specification and analysis of the IEEE token ring protocol proves the protocol won't fail for a two machine network. This thesis also proves that the specification of the protocol is correct. (kr)