Paper Info
Title
Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools
Abstract
The i-protocol, an optimized sliding-window protocol for GNU UUCP, came to our attention two years ago 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 repeated this verification effort with five widely used model checkers, namely, COSPAN, Murϕ, SMV, Spin, and XMC. It is our contention that the i-protocol makes for a particularly compelling case study in protocol verification and for a formidable benchmark of verification-tool performance, for the following reasons: 1) The i-protocol can be used to gauge a tool's ability to detect and diagnose livelock errors. 2) The size of the i-protocol's state space grows exponentially in the window size, and the entirety of this state space must be searched to verify that the protocol, with the livelock error eliminated, is deadlock- or livelock-free. 3) The i-protocol is an asynchronous, low-level software system equipped with a number of optimizations aimed at minimizing control-message and retransmission overhead. It lacks the regular structure that is often present in hardware designs. In this sense, it provides any verification tool with a vigorous test of its analysis capabilities.
Year
Venue
Keywords
1999
TACAS
verification tools,model checker,comparative study,diagnose livelock error,non-trivial livelock,fighting livelock,verification tool,verification effort,state space,livelock error,optimized sliding-window protocol,protocol verification,local model checker,sliding window,software systems
Field
DocType
Volume
Asynchronous communication,Model checking,Computer science,Concurrency,Network packet,Deadlock,Software system,State space,Embedded system,Distributed computing,Formal verification
Conference
1579
ISSN
ISBN
Citations 
0302-9743
3-540-65703-7
36
PageRank 
References 
Authors
2.00
11
9
Name
Order
Citations
PageRank
Yifei Dong120017.58
Xiaoqun Du222512.32
Y. S. Ramakrishna353445.81
C. R. Ramakrishnan41427107.75
I. V. Ramakrishnan51969214.75
Scott A. Smolka62959249.22
Oleg Sokolsky72193154.94
Eugene W. Stark8729120.29
David Scott Warren92447480.41