Information Technology Reference
In-Depth Information
memory occupation. This is done by storing only the states at depth n which are
not also at depth n
1. The space saving is paid in terms of precision, since miss-
ing the memory of visited states reduces convergence. Indeed, a non-monotonic
exploration diverges on correct programs (even finite-state ones) with at least
an infinite computation with cycle length greater than 1. As an example, the C
program while ( 1 )
{
x := x + 1 ;
}
diverges this way.
ExploreTesting( p , I , O ):
S
S
s.t. S ⊆ I
S
:= choose
and
is finite
exact := ( S = I )
loop:
if
S ⊆ O
return INCORRECT
S := s∈S choose s s.t. s Post( p, {s} )
exact := exact ( S =Post( p, S ))
if
S ⊆ S :
if exact return CORRECT else return INCONCLUSIVE
S − S
S
:=
Fig. 4. State space exploration by means of testing
Figure 4 summarizes how testing explores the state space. Testing starts from
a finite set of initial states (test cases), and for each of them at each step chooses
exactly one successor to explore. These can be seen as a both non-monotonic and
width-bounded exploration (bound = 1). Testing does not bound the depth of
execution, and thus may diverge. An interesting observation is that, differently
from purely non-monotonic and purely width-bounded explorations, testing may
converge with inconclusive answers. This can happen because, when sampling
discards a state, this is lost because of non-monotony.
3.3 Exploring via Auxiliary Spaces
The approaches summarized in the former section deal with the state explosion
problem by limiting the set of examined states, thus producing partial results.
Another class of approaches handles infinity directly either in width by intension-
ality or in depth by abstraction. These approaches exploit the idea of recasting
the exploration in an auxiliary space, with better properties than the original
program state space.
Intensionality. Full exhaustive search strategies assume an extensional ( explicit-
state ) representation of sets of program states. Representing a set as the enu-
meration of its members requires the same storage size of the set that must be
represented. Consequently, the implementations of explicit-state approaches do
not scale with the size of the analyzed program, and cannot analyze exhaustively
programs with infinitely many reachable states. Intensional ( symbolic-state )ap-
proaches deal with the state explosion problem by describing sets of states that
 
Search WWH ::




Custom Search