Research Article Open Access

Formal Validation of the Safety Property of Sack Protocol Using Theorem Proving Technique

Z. Shukur1, N. Alias1, M. H. Mohamed Halip2 and B. Idrus1
  • 1 ,
  • 2 , Afganistan
Journal of Computer Science
Volume 3 No. 6, 2007, 449-453

DOI: https://doi.org/10.3844/jcssp.2007.449.453

Submitted On: 7 April 2007 Published On: 30 June 2007

How to Cite: Shukur, Z., Alias, N., Halip, M. H. M. & Idrus, B. (2007). Formal Validation of the Safety Property of Sack Protocol Using Theorem Proving Technique. Journal of Computer Science, 3(6), 449-453. https://doi.org/10.3844/jcssp.2007.449.453

Abstract

This paper demonstrates the formal validation process of safety properties of Selective ACKnowledgment (SACK) protocol. 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. One of the critical property of SACK is its’ safety property. In order to validate this property formally by using the Z/Eves theorem prover, we specify the SACK protocol using Z formal specification language. By using theorem prover tool, it helps to reduce time, energy and mistake than in relatively manual theorem proving which can be tedious and error-prone task.

  • 780 Views
  • 1,298 Downloads
  • 0 Citations

Download

Keywords

  • formal validation
  • Z specification
  • safety property
  • protocol communication
  • SACK