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

requires an ability to execute it. This is commonly referred to as unit-
testing.
6.6.3 Selection of Paths for Inspection
When a scenario is identified as spurious, the abstraction used for min-
ing can be locally refined to eliminate the spurious scenario. The question
remaining is how to identify spurious paths, namely, how to select paths for
inspection.
There are a number of approaches for selecting paths for inspection. The
naive approach is to simply try all acyclic paths in the mined automaton, or
some bounded unrolling of the cyclic paths. When the final result of mining
is a weighted automaton, spurious paths/edges may be identified as the ones
that have a relatively low weight.
Example 6.6.1. Consider the Signature API. Suppose that the mined au-
tomaton, mined with the past abstraction, is the one depicted in Figure 6.11(a).
We now enumerate all acyclic paths in the mined automaton of Figure 6.11(a):
(ii) initSign;update;sign;initSign
(ii) initSign;update;verify;initVerify
(iii) initVerify;update;verify;initVerify
(iv) initVerify;update;sign;initSign
We now run inspection, say static client-side inspection (typestate verifica-
tion), to verify the absence of each one of the sequences (i)-(iv). This is done
by specifying the sequence itself as an input typestate property for the verifier.
Since the typestate verifier does not need to record histories, we can employ
the solver with more precise abstractions, and observe the fact that both (ii)
and (iv) are sequences that cannot occur in the client program.
Based on this information, we can locally increase the context for the past
abstraction such that it is able to distinguish the valid sequences (i) and (iii)
from the invalid ones (ii) and (iv).
6.6.4 Refinement Based on Abstraction Merge Points
A more sophisticated approach for refinement, which also uses inspection,
is based on the merge points of the abstraction. Recall that our past-future ab-
stractions merge automata states based on their ingoing/outgoing sequences.
These merge points are responsible for the over-approximation of the spec-
ification. As such, we aim at identifying merge points which are potentially
responsible for the inclusion of spurious behaviors.
Consider the past abstraction. Similar ideas are applicable for the future
abstraction as well. In the k-past abstraction, an automaton state q that
has (at least) two ingoing paths of length k labeled with the same sequence