Formal validation of the safety property of sack protocol using theorem proving technique

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. Key words: formal validation, Z specification, safety property, protocol communication, SACK
INTRODUCTION Communication protocol is a complex protocol and it is used in many distributed system and networks. Non-formal techniques are successfully used to design the protocol, but it contains unexpected [...]