Sciweavers

SPIN
2010
Springer

Context-Enhanced Directed Model Checking

13 years 2 months ago
Context-Enhanced Directed Model Checking
Directed model checking is a well-established technique to efficiently tackle the state explosion problem when the aim is to find error states in concurrent systems. Although directed model checking has proved to be very successful in the past, additional search techniques provide much potential to efficiently handle larger and larger systems. In this work, we propose a novel technique for traversing the state space based on interference contexts. The basic idea is to preferably explore transitions that interfere with previously applied transitions, whereas other transitions are deferred accordingly. Our approach is orthogonal to the model checking process and can be applied to a wide range of search methods. We have implemented our method and empirically evaluated its potential on a range of non-trivial case studies. Compared to standard model checking techniques, we are able to detect subtle bugs with shorter error traces, consuming less memory and time.
Martin Wehrle, Sebastian Kupferschmid
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where SPIN
Authors Martin Wehrle, Sebastian Kupferschmid
Comments (0)