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

up

initS

1' 3'

initS

1' 2' 3' 4'

initS up sign initS

up sign

0

0

2

up verify

up verify initV

initV

3

initV

1

1 2 3 4'

initV

up

(a) (b)

FIGURE 6.11: (a) 1-Past abstraction; and (b) 2-Past abstraction.

(at least) two ingoing paths labeled with the same sux of length k (due to
the past-property). For example, in Figure 6.11(a), state 2 has two ingoing
transitions, and indeed these represent two ingoing paths labeled with the
same sux of length 1.
Note that the full sequences that label the ingoing paths that lead from
the initial state to such a state cannot be identical, although they end with
an identical sux. This is because at latest the ingoing paths collide at the
initial state, and since the automaton is deterministic, the transitions where
the paths collide must be labeled by different events. In the above example
the ingoing paths of state 2 collide at the initial state and the corresponding
transitions are indeed labeled by different events: initSign and initVerify .
Moreover, the two different ingoing sequences can be found by a backward
traversal of the BFS tree until the initial state is encountered.
Let q be such an automaton state that has two different ingoing sequences.
To check if q also has at least two different outgoing behaviors (and find them),
another BFS is applied, starting from q. There are three possibilities.

(1) The search ends without finding any state with more than one outgoing
transition. In this case, no inspection is needed since q has only one
outgoing behavior, thus the merge did not add any behavior.

(2) The search reaches a state q 0 (possibly q itself) that has at least two
outgoing transitions. In this case, the path from q to q 0 followed by the
two outgoing transitions of q 0 defines two different outgoing behaviors of
q. This is the case in Figure 6.11(a), where state 2 itself has two outgoing
transitions: one labeled sign and one labeled verify .

(3) The search reaches a previously visited state q 0 . This means that a simple
loop was encountered, one that has no outgoing transitions (except for
the ones along the loop). In this case different unwindings of the loop
define different behaviors that originate in q.

Similar ideas can be used on the nondeterministic automata returned by
future merge.