Title of article :
Penspesifikasian dan Pengesahsahihan Formal Protokol CSMA/CD Menggunakan Z
Author/Authors :
Shukur, Zarina Universiti Kebangsaan Malaysia - Fakulti Teknologi dan Sains Maklumat - Jabatan Sains Komputer, Malaysia , Alias, Nursyahidah Universiti Kebangsaan Malaysia - Fakulti Teknologi dan Sains Maklumat - Jabatan Sains Komputer, Malaysia , Idrus, Bahari Universiti Kebangsaan Malaysia - Fakulti Teknologi dan Sains Maklumat - Jabatan Sains Komputer, Malaysia , Mohamed Halip, Mohd Hazali Universiti Kebangsaan Malaysia - Fakulti Teknologi dan Sains Maklumat - Jabatan Komputeran Industri, Malaysia
Abstract :
This paper discusses the formal specification and validation for CSMA/CD protocol. The Z specification language is used to specify a node in a network and a situation in a bus implementation for CSMA/CD protocol. One basic type, four free types, one global variables, two state schemas and nine operation schemas that represent CSMA/CD protocol have been specified by using the Z language. The specification has been validated by using theorem proving techniques supported by Z/EVES theorem prover. Nine theorems have been identified based on the nine specified operations. This study has shown that, Z has the ability to specify a communication protocol. Beside that, the usage of support tools during a proving process can save time dan energy and reduce error-prone.
Keywords :
Formal specification , Z , Z , EVES , network protocol
