A program which takes as input the formal specification of a protocol using the formal model systems of communicating machines, and outputs a sequence of tests for an implementation of the protocol is discussed. The protocol is specified formally as a finite state machine with local and shared variables. The test program, called TESTGEN, finds all paths which may be taken through the FSM and generates a sequence of tests to check all these paths. Certain possible error conditions or difficult to test conditions are also detected by the program, and the test designer receives a warning message. The program is applied to a formal specification of the CSMA/CD and FDDI protocols, generating a test sequence for both of these protocols.>

The emergence of optical fiber and its correspondingly high data rates have led to the development of much higher speed networks, both locally and over the long haul. These developments led to the design of new transport protocols, which were intended to take advantage of the high-speed networks. A number of these so-called "high-speed transport protocols" have been designed to date. This paper considers one of these, called the SNR protocol, in detail. A formal specification of the protocol is presented, using the protocol model systems of communicating machines, and the protocol is then analyzed through the specification. An implementation of the protocol based on this formal definition has also been made, and used to simulate the protocol, providing further insights into its performance. Based on the combined results of the analysis and the simulated protocol, a high degree of confidence is gained in the correctness of the protocol. The specification is quite detailed, and from it an implementation should be fairly straightforward. The paper also discusses the difficulties encountered during the analysis of such a complex protocol, and suggests some possible solutions to these problems. Finally, as a result of this work, we comment on the strengths and weakness of the SNR protocol as a solution to the high-speed transport protocol problem, and make two simple suggestions for improving it.>

Systems of communicating machines (SCM) is a formal model for the specification, verification and testing of communication protocols, which has been used to specify and verify several well-known protocols. The authors discuss a program, called mushroom, which automates the analysis using the SCM model. The program generates either the system state analysis or the full reachability analysis. The automation of this model is expected to greatly facilitate the use of the model for protocol design and analysis. The program has been used to verify some theoretical results, serving to confirm these earlier results.>

A model for the specification and analysis of communication protocols called Systems of Communicating Machines is used to specify a CSMA/CD (carrier-sense multiple access with collision detection) protocol, and to analyze it for safety and certain restricted liveness properties. The model uses a combination of finite state machines and variables in the specification of each machine, and the communication between machines is accomplished through shared variables. The Ethernet bus is modeled as a single variable shared by all communicating processes. Collisions are modeled by simultaneous writes to this variable.>