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 to detect, locate, and correct a non-trivial livelock in version 1.04 of the protocol. Since then, we have conducted a systematic case study on the protocol using four verification tools, viz. Cospan, Murφ, Spin, and XMC, each of which supports some form of explicit-state model checking. Our results show that although the i-protocol is inherently complex - the size of its state space grows exponentially in the window size and it deploys several sophisticated optimizations aimed at minimizing control-message and retransmission overhead - it is nonetheless amenable to a number of general-purpose abstraction techniques whose application can significantly reduce the size of the protocol's state space. © 2002 Springer-Verlag.
CITATION STYLE
Dong, Y., Du, X., Holzmann, G. J., & Smolka, S. A. (2003). Fighting livelock in the GNU i-protocol: A case study in explicit-state model checking. International Journal on Software Tools for Technology Transfer, 4(4), 505–528. https://doi.org/10.1007/s10009-002-0092-3
Mendeley helps you to discover research relevant for your work.