Transition-Based Directed Model Checking

12 years 6 months ago
Transition-Based Directed Model Checking
Abstract. Directed model checking is a well-established technique that is tailored to fast detection of system states that violate a given safety property. This is achieved by influencing the order in which states are explored during the state aversal. The order is typically determined by an abstract distance function that estimates a state’s distance to a nearest error state. In this paper, we propose a general enhancement to directed model checking based on the evaluation of state ons. We present a schema, parametrized by an abstract distance function, to evaluate transitions and propose a new method for the state space traversal. ework can be applied automatically to a wide range of abstract distance functions. The empirical evaluation impressively shows its practical potential. Apparently, the new method identifies a sweet spot in the trade-off between scalability (memory consumption) and short error traces.
Martin Wehrle, Sebastian Kupferschmid, Andreas Pod
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Authors Martin Wehrle, Sebastian Kupferschmid, Andreas Podelski
Comments (0)