Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking |
| |
Authors: | Yifei Dong Xiaoqun Du Gerard J Holzmann Scott A Smolka |
| |
Affiliation: | (1) Department of Computer Science, SUNY at Stony Brook, NY 11794–4400 Stony Brook, USA;(2) Cadence Design Systems, 35 Spring Street, NJ 07974 New Providence, USA;(3) Bell Laboratories, 600 Mountain Avenue, NJ 07974 Murray Hill, USA |
| |
Abstract: | The i-protocol, an optimized sliding-window protocol for GNU uucp, first came to our attention in 1995 when we used the Concurrency Factorys 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 protocols state space. |
| |
Keywords: | Explicit-state model checking Livelock Protocol verification Sliding-window protocol |
本文献已被 SpringerLink 等数据库收录! |
|