Analyzing a CSMA/CD protocol through a Systems of Communicating Machines Specification

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