Formal specification and validation of selective acknowledgement protocol using Z/EVES theorem prover

Zarina Shukur, Nursyahidah Alias, Mohd Hazali Mohamed Halip, Bahari Idrus

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

Selective ACKnowledgment (SACK) is a complex communication protocol as it is used in various types of distributed computer systems and networks. This acknowledgment mechanism is used with sliding window protocol that allows the receiver to acknowledge packets received out of order, but within the correct sliding window. In this study the SACK protocol has been specified by using Z formal specification language. A formal Z specification provides validation function to ensure that the specification is complete and consistent. The completeness and consistency of Z specification can be checked by proving initial state theorem, pre-condition and properties of a system specification. This study demonstrates the validation process of Z specification of SACK by using theorem proving technique. A theorem prover toot called Z/EVES is used to support the process. It helps to reduce time, energy and mistake than in relatively manual theorem proving which can be tedious and error-prone task.

Original languageEnglish
Pages (from-to)1712-1719
Number of pages8
JournalJournal of Applied Sciences
Volume6
Issue number8
DOIs
Publication statusPublished - 17 Jul 2006

Fingerprint

Specifications
Network protocols
Theorem proving
Specification languages
Distributed computer systems
Computer networks
Formal specification

Keywords

  • Formal specification
  • Formal validation
  • Protocol communication
  • Safety property

ASJC Scopus subject areas

  • General

Cite this

Formal specification and validation of selective acknowledgement protocol using Z/EVES theorem prover. / Shukur, Zarina; Alias, Nursyahidah; Halip, Mohd Hazali Mohamed; Idrus, Bahari.

In: Journal of Applied Sciences, Vol. 6, No. 8, 17.07.2006, p. 1712-1719.

Research output: Contribution to journalArticle

@article{f833b89fa5a34c8cb46daee0a37a4194,
title = "Formal specification and validation of selective acknowledgement protocol using Z/EVES theorem prover",
abstract = "Selective ACKnowledgment (SACK) is a complex communication protocol as it is used in various types of distributed computer systems and networks. This acknowledgment mechanism is used with sliding window protocol that allows the receiver to acknowledge packets received out of order, but within the correct sliding window. In this study the SACK protocol has been specified by using Z formal specification language. A formal Z specification provides validation function to ensure that the specification is complete and consistent. The completeness and consistency of Z specification can be checked by proving initial state theorem, pre-condition and properties of a system specification. This study demonstrates the validation process of Z specification of SACK by using theorem proving technique. A theorem prover toot called Z/EVES is used to support the process. It helps to reduce time, energy and mistake than in relatively manual theorem proving which can be tedious and error-prone task.",
keywords = "Formal specification, Formal validation, Protocol communication, Safety property",
author = "Zarina Shukur and Nursyahidah Alias and Halip, {Mohd Hazali Mohamed} and Bahari Idrus",
year = "2006",
month = "7",
day = "17",
doi = "10.3923/jas.2006.1712.1719",
language = "English",
volume = "6",
pages = "1712--1719",
journal = "Journal of Applied Sciences",
issn = "1812-5654",
publisher = "Asian Network for Scientific Information",
number = "8",

}

TY - JOUR

T1 - Formal specification and validation of selective acknowledgement protocol using Z/EVES theorem prover

AU - Shukur, Zarina

AU - Alias, Nursyahidah

AU - Halip, Mohd Hazali Mohamed

AU - Idrus, Bahari

PY - 2006/7/17

Y1 - 2006/7/17

N2 - Selective ACKnowledgment (SACK) is a complex communication protocol as it is used in various types of distributed computer systems and networks. This acknowledgment mechanism is used with sliding window protocol that allows the receiver to acknowledge packets received out of order, but within the correct sliding window. In this study the SACK protocol has been specified by using Z formal specification language. A formal Z specification provides validation function to ensure that the specification is complete and consistent. The completeness and consistency of Z specification can be checked by proving initial state theorem, pre-condition and properties of a system specification. This study demonstrates the validation process of Z specification of SACK by using theorem proving technique. A theorem prover toot called Z/EVES is used to support the process. It helps to reduce time, energy and mistake than in relatively manual theorem proving which can be tedious and error-prone task.

AB - Selective ACKnowledgment (SACK) is a complex communication protocol as it is used in various types of distributed computer systems and networks. This acknowledgment mechanism is used with sliding window protocol that allows the receiver to acknowledge packets received out of order, but within the correct sliding window. In this study the SACK protocol has been specified by using Z formal specification language. A formal Z specification provides validation function to ensure that the specification is complete and consistent. The completeness and consistency of Z specification can be checked by proving initial state theorem, pre-condition and properties of a system specification. This study demonstrates the validation process of Z specification of SACK by using theorem proving technique. A theorem prover toot called Z/EVES is used to support the process. It helps to reduce time, energy and mistake than in relatively manual theorem proving which can be tedious and error-prone task.

KW - Formal specification

KW - Formal validation

KW - Protocol communication

KW - Safety property

UR - http://www.scopus.com/inward/record.url?scp=33749647733&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33749647733&partnerID=8YFLogxK

U2 - 10.3923/jas.2006.1712.1719

DO - 10.3923/jas.2006.1712.1719

M3 - Article

VL - 6

SP - 1712

EP - 1719

JO - Journal of Applied Sciences

JF - Journal of Applied Sciences

SN - 1812-5654

IS - 8

ER -