Abstract
-
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.