Using compositional preorders in the verification of sliding window protocol

The main obstacle to automatic verification of temporal logic properties of finite-state systems is the state explosion problem. One way to alleviate this is to replace components of a system with smaller ones and verify the required properties from the smaller system. This approach leads to notions of compositional property-preserving equivalences and preorders. Previously we have shown that the NDFD preorder is the weakest preorder which is compositional w.r.t. standard operators and preserves nexttime-less linear temporal logic properties. In this paper we describe a case study where NDFD preorder was used to verify semiautomatically both safety and liveness properties of the Sliding Window protocol for arbitrary channel lengths and realistic parameter values. In this process we located a previously undiscovered fault leading to lack of liveness in a version of the protocol.