Information Technology Reference
In-Depth Information
Input
:(
)
LT S ← generateAPTA
(
Pos,Neg
);
Pos,Neg
1
while
(
q, q
)
← selectStateP air
(
LT S
)
do
2
LT S
← merge
(
PLTS,
(
q, q
));
3
if
Compatible
(
PLTS
,Pos,Neg
)
then
4
LT S ← LT S
;
5
end
6
end
7
return
LT S
8
Algorithm 1.
EDSM algorithm
executions, and a set
Neg
of traces that represent either infeasible executions,
or executions that terminate with an exception or failure
4
. These traces are first
arranged into a tree-structured state machine that exactly accepts the given
set of traces (this is referred to as an
Augmented Prefix Tree Acceptor
). In the
algorithm this is carried out by the
generateAPTA
function in line 1. The
process of inferring the state machine subsequently consists of repeating the
following process: A pair of states that are deemed to be equivalent is selected,
(2) the pair is merged, and (3) the resulting machine is checked against
Pos
and
Neg
to ensure that it is still compatible - if not the merge is ignored. The
process terminates when no further mergable state-pairs are found.
The key to the effectiveness of the EDSM algorithm is the
selectStateP air
function. It does not simply select the first pair of states that are deemed to
be compatible. It computes a “similarity score” for each pair, and then merges
pairs in the order of their scores (highest to lowest). The similarity score is
computed by counting the extent to which their outgoing paths overlap with each
other. The greater the overlap, the greater the score. Thanks to the availability
of negative traces, it is also possible to rule-out state merges if they have a
conflicting set of outgoing paths (i.e. a sequence is deemed to be possible from
one state but not from another). If this is the case, the pair is assigned a score
of -1 to prevent a merge from occurring.
The
merge
function (Line 3) takes two states
q
and
q
, along with the current
state machine
A
.Ineffect,thestate
q
is removed, all of its incoming transitions
are routed to
q
instead and all of its outgoing transitions are routed from
q
.
Every time a pair of states is merged, the resulting state machine may be non-
deterministic. Nondeterminism is eliminated by recursively merging the targets
of non-deterministic transitions.
A comprehensive description of the EDSM algorithm itself is beyond the scope
of this paper, and the reader is referred to the original paper by Lang
et al.
[17] for a
more complete description. In practice, our implementation does not compare
ev-
ery
pair of states at any given point. It uses a windowing-strategy to compare only
4
Traditional dynamic analysis approaches presume that all traces represent positive
/ valid executions. However, in our work, traces that lead to a program failure (i.e.
an exception) are interpreted as “invalid” and so added to the
Neg
set in the EDSM
algorithm.
