Specification and Verification of Sliding Window Protocol Using Predicate Logic
A number of protocol verification reduction techniques were proposed in the past. Most of these techniques are suitable for verifying communicating protocols specified in the Communicating Finite State Machine (CFSM) model. However, it is impossible to formally specify communicating protocols with variables using the CFSM model. Also these methods suffered from the problem of state exploration. In this paper, the authors have proposed a technique that used the predicate logic for specification and verification of sliding window protocol. This method is based on the technique that between sender and receiver an action is defined for any transition rule also guards and post-conditions respectively corresponding to that transition rule.