Static Specification Mining Using Automata-Based Abstractions* - Mining Software Specifications: Methodologies and Applications - page 184

represents a merge point. The joint sux of length k of the two ingoing paths
is responsible for the merge of the states that resulted in q. For example, in
Figure 6.11(a), state 2 is a merge point of the past abstraction as it has two
ingoing sequences ( initSign;update , initVerify;update ). The sux update
of these sequences is responsible for the merge.
If the state q that represents a merge point also has (at least) two different
outgoing behaviors, then this means that one originated while tracking the
first ingoing sequence and the second originated when tracking the other. The
merge introduced the additional two combinations of ingoing and outgoing
sequences.
For example, in Figure 6.11(a), state 2 has two outgoing sequences: sign
which originated after tracking the ingoing sequence initSign;update , and
verify which originated after tracking the ingoing sequence initVerify;
update . The merge introduced the (erroneous) combinations of initSign;
update and verify and of initVerify;update and sign .
States that have multiple ingoing and outgoing sequences are therefore
considered suspicious merge points and are candidates for inspection. When a
suspicious merge point q is encountered, the validity of the merge is inspected
by checking if all the combinations of an ingoing sequence and an outgoing
sequence are legitimate.
If one of these combinations turns out to be illegal, refinement of q is
needed. This can be achieved by increasing the context of the past abstraction
to reflect the difference between the two ingoing sequences of q.
Example 6.6.2. Consider the Signature API. Suppose that the mined au-
tomaton, mined with the past abstraction, is the one depicted in Figure 6.11(a).
In this case, state 2 is a suspicious merge point as it has both two different
ingoing sequences ( initSign;update , initVerify;update ) and two outgoing
sequences ( sign , verify ). Indeed, inspection shows that the concatenation of
initSign;update and verify , as well as the concatenation of initVerify;
update and sign , results in a spurious path. Thus, refinement increases the
context of the past abstraction to 2, as length 2 reflects the difference between
the ingoing sequences of state 2. This prevents the spurious merge and the
resulting automaton is depicted in Figure 6.11(b).
Note, however, that this kind of refinement does not guarantee that the
\bad" state q will be split in the next iteration of mining (with the extended
context), since there can be other ingoing sequences of the increased length
that will cause q to be merged again. For example, if in the Signature example
state 2 has a selfloop with the update event (i.e., the code base allows any
number of update events before verify or sign ), then no finite context will
prevent the merge.
Suspicious merge points are found as follows. First, an automaton state
that has (at least) two ingoing paths labeled with the same sequence of length
k is found by a BFS from the initial state. Whenever a new state is encoun-
tered, we check if it has at least two ingoing transitions. If it does, then it has