Improving Non-Progress Cycle Checks

10 years 6 months ago
Improving Non-Progress Cycle Checks
This paper introduces a new model checking algorithm that searches for non-progress cycles, used mainly to check for livelocks. The algorithm performs an incremental depth-first search, i.e., it searches through the graph incrementally deeper. It simultaneously constructs the state space and searches for non-progress cycles. The algorithm is more efficient than the method the model checker SPIN currently uses, and finds shortest (w.r.t. progress) counterexamples. Its only downside is the need for a subsequent reachability depth-first search (which is not the bottleneck) for constructing a full counterexample. The new algorithm is better combinable with partial order reduction than SPIN’s method. Key words: Model Checking, SPIN, Non-progress cycles, livelocks, depthfirst search, partial order reduction.
David Faragó, Peter H. Schmitt
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SPIN
Authors David Faragó, Peter H. Schmitt
Comments (0)