%0 Journal Article
%T Formal Specification and Verification of CSMA/CD Protocol Using Z
%A Zarina Shukur
%A Nursyahidah Alias
%A Bahari Idrus
%A Mohd Hazali Mohamed Halip
%J Jurnal Kejuruteraan
%D 2009
%I 
%X 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.
%K Formal specification
%K Z
%K Z/EVES
%K network protocol.
%U http://pkukmweb.ukm.my/~jkukm/2009-9.pdf