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.

• Type: Conference
• Year: 2009
• Where: TACAS
• Authors: Martin Wehrle, Sebastian Kupferschmid, Andreas Podelski
• Keywords: Abstract Distance Functions, Algorithms, Model Checking, Nearest Error State, TACAS 2009