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.

• Type: Conference
• Year: 2009
• Where: SPIN
• Authors: David Faragó, Peter H. Schmitt
• Keywords: Algorithm, Model Checking Algorithm, Non-progress Cycles, SPIN 2009, Theoretical Computer Science