Information Technology Reference
In-Depth Information
1
ExploreDASH(
p
,
I
,
O
):
2
H
{init, ok}
O
H
{{init, ok}, {ok}}
:=
;
:=
S
H
:=
S
H
3
S
I
⊆
S
sy
{
(id
,init
)
}
:=
;
:=
;
4
init, ok ∈
E
s.t.
init
=
I
,
ok
=
O
where
5
loop:
6
S ⊆ O
if
return INCORRECT
S
:=
Post(
p, S
)
⊆
S
H
S
H
7
;
:=
S
⊆ S
:
8
if
9
S
H
O
H
:
if
S
H
10
:=
Post
H
(
p, S
H
)
S
H
S
H
11
if
return CORRECT
12
else:
φ
:=
sp(
p, φ
)
13
φ
S
sy
:=
;
:=
(
S
H
∧¬
S
H
)
⇒
14
φ
new
S
:=
φ
∧ φ
new
⊆
S
H
S
H
15
;
:=
S
=
∅
:
16
if
17
r
:=
¬
wlp(
p, ¬φ
new
)
;
H
H ∪{r}
:=
18
O
H
{σ ∈P
(
H
)
| ok ∈ σ}
:=
S
H
19
S
H
:=
S
sy
:=
Post
co
(
p, S
sy
,S
)
20
S
∪ S
S
sy
S
sy
S
H
S
H
21
S
S
sy
S
H
:=
;
:=
;
:=
Fig. 13.
Dash
φ
⇒
=
⇒
φ,
φ
≡
false
implies
φ
⇒
≡
false.
Strengthening reflects the previous informal description of Dash,whereonlya
single abstract error trace, rather than the whole frontier, is considered for test
case generation. The region
φ
∧
φ
new
is abduced to concrete execution (line 15).
If abduction does not progress the analysis, then no successor of a state in
S
sy
can
support the abstract states in
φ
new
. Dash exploits this information to refine the
model by adding a refinement predicate, i.e., the weakest precondition of
φ
new
,
to
H
(line 17). The refinement predicate is satisfied by all (and only) the states
with no successors in
φ
new
. Figure 13 does not highlight the fact that Dash
calculates Post
H∪{r}
syntactically, i.e., without invoking a theorem prover. More
precisely, it splits the abstract states along
r
, it replicates Post
H∪{r}
on all the
split states, and then it cancels all the transitions from the abstract states where
r
is false, to abstract states where
φ
new
is true. While this is an especially limited
form of refinement, it has the advantage of being computationally inexpensive,
and is sucient to ensure that test case generation will not retry to support
these abstract states along the same frontier.
In Dash any discovered symbolic state is always supported by at least one con-
crete state (as in concolic execution), and any discovered abstract states may be
supported or not (but during testing surely is) by a concrete state. In formulas:
¬
S
sy
H
S
=
S
sy
,
S
S
H
,
Search WWH ::
Custom Search