On the Integration of Software Testing and Formal Analysis - Empirical Software Engineering and Verification - page 184

s s

ªº

V

r

ªº

V

r

ªº

V

ªº

V

ªº

V

(a) (b)

Fig. 12. Refining an infeasible transition (Abstract states are annotated with the pred-
icates signifying their extensions)

the reachability of σ 2 is reduced to the problem of proving the reachability of
r

.When σ 2 is unreachable, subsequent iterations of Dash may propagate
the frontier back beyond the entry state of the model. In such case, Dash safely
concludes that such a frontier is infeasible and safely removes the frontier edge
from the model without splitting the source node.
Figure 13 illustrates the Dash approach by considering predicate abstraction
as the framework for abstraction refinement. The abstraction captures the sets
of initial and error states, by including two predicates init and ok with extension
I and O respectively. Similarly to concolic execution and to the Yorsh-Ball-
Sagiv procedure, Dash starts from a set of random test cases, executes them,
and collects the corresponding reachable symbolic and abstract states exploiting
the feeding of reachable states (FRS) synergy (lines 7 and 20 in Figure 21). If
testing reveals an error state, Dash terminates signaling INCORRECT (line 6).
Otherwise, Dash explores exhaustively the abstract space (lines 9-11) starting
from the region discovered through the FRS synergy. This exploration builds
either a safe invariant in S H or an abstract region that contains an error state.
In the first case Dash concludes with CORRECT (line 11), in the latter case,
Dash progresses (lines 12-19), since neither testing nor abstract verification
have produced a conclusive answer yet.
In Dash, test case generation and refinement exploit S H to guarantee that the
analysis progresses towards the final goal. Test case generation progresses the
search towards a reachable error state by generating a test case that traverses
at least an abstract state in S H (not necessarily the abstract error state) that
has not been already traversed by some state in S . Such constraint is expressed
by a predicate φ new that is conjoined to the symbolic post-states to be explored
(line 15, left part). φ new is defined in line 14 as any predicate which is nontrivial
(whenever possible) and stronger than the whole uncovered abstract region. We
introduce at the purpose a strengthening function (

∧ σ 1

− ) ⇒ , enjoying the same

properties as sampling: