Journal of Computer Science

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

Z. Shukur, N. Alias, M. H. Mohamed Halip and B. Idrus

DOI : 10.3844/jcssp.2007.449.453

Journal of Computer Science

Volume 3, Issue 6

Pages 449-453


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.


© 2007 Z. Shukur, N. Alias, M. H. Mohamed Halip and B. Idrus. This is an open access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.