Similarity-based search for model checking: a pilot study with java pathfinder

When a model checker cannot explore the entire

state space because of limited resources, model checking becomes

a kind of testing with an attempt to find a failure (violation of

properties) quickly. We consider two state sequences in model

checking: (i) the sequence in which new states are generated, and

(ii) the sequence in which the states generated in sequence (i) are

checked for property violation. We observe that neighboring

states in sequence (i) often have similarities in certain ways.

Based on this observation we propose a search strategy, which

generates sequence (ii) in such a way that similar states are

evenly spread over the sequence. As a result, neighboring states

in sequence (ii) can have a higher diversity. A pilot empirical

study with Java PathFinder suggests that the proposed strategy

can outperform random search in terms of creating equal or

smaller number of states to detect a failure.