Formal Specification and Verification of CSMA/CD Protocol Using Z

This paper discusses the formal specification and validation for CSMA/CD protocol. The Z specificationlanguage is used to specify a node in a network and a situation in a bus implementation for CSMA/CDprotocol. One basic type, four free types, one global variables, two state schemas and nine operation schemasthat represent CSMA/CD protocol have been specified by using the Z language. The specification has beenvalidated by using theorem proving techniques supported by Z/EVES theorem prover. Nine theorems havebeen identified based on the nine specified operations. This study has shown that, Z has the ability to specifya communication protocol. Beside that, the usage of support tools during a proving process can save timedan energy, and reduce error-prone.