Information Technology Reference
In-Depth Information
Explore(
p
,
I
,
O
):
--
p
is a program , a set of statements
(
f, g
)
I
--
is the set of initial states
O
--
is the set of safe states
S
I
:=
loop:
if
S ⊆ O
return INCORRECT
S
:=
Post(
p, S
)
if
S
⊆ S
return CORRECT
S
∪ S
S
:=
Fig. 2.
Full exhaustive state space exploration
Figure 2 drafts the skeleton of the approach to full exhaustive state space
exploration, which can be considered either the ideal exhaustive testing (if the
program is deterministic) or explicit-state model checking (if the program is non-
deterministic)
1
. The procedure relies on the definition of the
post-states trans-
former
Post :
P
×P
(
S
) that is defined as:
Post(
p, S
)
de
=
s∈S
(
S
)
→P
s
p
s
∈
s
}
{
S
|
→
for
S
⊆
S
.
Intuitively, Post(
p, S
) contains all and only the successors of some state in
S
,ac-
cording to
p
. The reachable state space of
p
starting fron
I
is
k≥
0
Post
k
(
p, I
),
where Post
0
(
p, I
)
de
=
I
and Post
k
+1
(
p, I
)
de
=Post(
p,
Post
k
(
p, I
)) . This can be seen
as the least fixpoint of the function
2
f
(
S
)
de
=Post(
p, S
)
→
(
S
). The
procedure calculates this fixpoint by iterating through a loop which, at the
n
-th
iteration, calculates into the variable
S
the underapproximation of the reachable
∪
I
:
P
(
S
)
→P
state space
0
≤k<n
Post
k
(
p, I
) and performs two termination checks. The loop is
structured as follows:
Check for failure:
if
S
contains a failure state, the procedure stops and returns
INCORRECT
;
Compute successors:
the successors of
S
are calculated and stored in
S
;
Check for success:
if all the successors are already in
S
, then the whole state
space has been explored without finding a failure state: The procedure stops
and returns
CORRECT
;
Update the computation state:
The successors are added to
S
, yielding
Post
k
(
p, I
)
.
0
≤k<n
+1
1
A program is
deterministic
whenever
|
Post(
p, {s}
)
|≤
1.
2
The fact is easily proved by taking into account that Post preserves union, i.e.,
Post(
p, S ∪ S
)=Post(
p, S
)
∪
Post(
p, S
).
Search WWH ::
Custom Search