Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking

摘要: The i-protocol, an optimized sliding-window protocol for GNU uucp, first came to our attention in 1995 when we used the Concurrency Factory’s local model checker detect, locate, and correct a non-trivial livelock version 1.04 of protocol. Since then, have conducted systematic case study on using four verification tools, viz. Cospan, Murϕ, Spin, XMC, each which supports some form explicit-state checking. Our results show that although i-protocol is inherently complex – size its state space grows exponentially window it deploys several sophisticated optimizations aimed at minimizing control-message retransmission overhead nonetheless amenable number general-purpose abstraction techniques whose application can significantly reduce protocol’s space.