Static API Specification Mining: Exploiting Source Code Model Checking - Mining Software Specifications: Methodologies and Applications - page 123

be the API invocations along the trace t expressed as a string. A(t) can be
an empty string if t does not have any invocation of APIs from the set A.
Let T 0 T be the set of all feasible traces such that if t2T 0 , A(t) is not empty.
However, the set T 0 is uncomputable and t2T 0 can be of infinite size. Our
framework initially does the following steps:

Generate the computable approximation of T 0 from the program and
extract A(t) for all t in the approximate set. The extracted A(t)'s are
stored in a string database, say, V .

Extract the set of FCPOs among APIs in A from V , with respect to a
minimum threshold min sup.

The high-level overview of our framework is shown in Figure 5.4. Our
framework has three main components: trace generator, scenario extractor,
and specification miner. The user specifies a set of APIs from which Triggers
(explained in Section 5.2.2.4) are generated. The Triggers are then used with
push-down model checking for trace generation. This process also recommends
more APIs related to the user-specified set of APIs. The scenario extractor
extracts various API scenarios (explained in Section 5.2.2.5) from the traces.
The specification miner feeds the extracted scenarios to a FCPO miner [47]
to output specifications and usage scenarios as partial orders. Each process is
described in detail in the subsections below. We first explain the process of
trace generation.

5.2.2.4 Trace Generation

We first briefly summarize the Push-Down Model Checking (PDMC) pro-
cess [18, 26], which we adapt for trace generation. To generate API invoca-
tion sequences along different program paths, we introduce the concept of
Triggers. Finally, we discuss the soundness of our framework.
Push-Down Model Checking (PDMC): Informally, given a property
represented using a Finite State Machine (FSM), PDMC [26] checks to see
if there is any path in the program that puts the FSM in its final state. For
example, if the property FSM is specified as shown in Figure 5.5, PDMC
reports all program paths in which a is followed by either b or c . PDMC
models the program as a Push Down Automata (PDA) and the property as
an FSM. PDMC then combines the program PDA and the property FSM
to generate a new PDA; the new PDA is then model checked to see if any
final configuration in the PDA is reachable. A configuration of a PDA P is
a pair c = hq;!i, where q is the state in which the PDA is in and ! is a
string of stack symbols in the PDA stack at that state. A configuration is

direct API invocations. If this is not the case, for a given API, say a , we have to consider all
the program statements that aect and are aected by a through some data-ow dependen-
cies. For example, if we have i=a(j);if(i!=NULL)b(i); , then the program
statements if(i!=NULL) and b(i) are related to a . We relax this assumption to a
certain extent later in the section by incorporating simple data-flow analysis.