A specification and analysis of the IEEE token bus protocol
Loading...
Authors
Charbonneau, Lauren J.
Subjects
Token bus protocol
systems of communicating machines
systems state analysis
systems of communicating machines
systems state analysis
Advisors
Lundy, G.M.
Date of Issue
1990-06
Date
June 1990
Publisher
Monterey, California. Naval Postgraduate School
Language
en_US
Abstract
In this thesis a formal description technique, systems of communicating machines, is used to specify and analyze a token bus protocol. A simplified description of the protocol is given, and proofs of certain correctness properties presented. The analysis proves that the protocol is free from deadlocks and non executable transitions, and also that successful message transfer is guaranteed for a network with an arbitrary number of machines. A program written in an object oriented language, C++, demonstrates that the description technique, the specification, and the analysis of the protocol is complete and accurate for a network of three stations. The specification is then extended to allow the transmission of different types of messages, errors in the communication channel, acknowledgements from the receiver, and timeouts.
Type
Thesis
Description
Series/Report No
Department
Department of Computer Science
Organization
Naval Postgraduate School (U.S.)
Identifiers
NPS Report Number
Sponsors
Funder
Format
iv, 82 p. ; ill.
Citation
Distribution Statement
Approved for public release; distribution is unlimited.
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.