Applying Event-B Refinement to the Sliding Window Protocol

The sliding window protocol (SWP) is a useful protocol in network communications. It can ensure a correct data transfer over unreliable channels where frames may be duplicated, lost, or re-ordered. This paper presents an incremental formal modeling of the SWP using Event-B method. We model the protocol step by step by using refinement, a technique of Event-B. The first step will be the modeling of the most abstract specification of the protocol. Then by each refinement more details of the protocol specification will be added to the model. By this approach, the model will be a more explicit representation of the target protocol by each refinement. Through a refinement approach, we prove that the abstract goals concerning sending and receiving windows of different size of the SWP are satisfied. In the developed Event-B models of the SWP described in this paper, all proofs are generated and discharged by the Rodin tool.