Specification and Analysis of the IEEE Token Bus Protocol

摘要

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 are 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.