Automatic Inference and Effective Application of Temporal Specifications - Mining Software Specifications: Methodologies and Applications - page 274

FIGURE 8.18: Inferred properties versus the acceptance threshold for p AL .

Figure 8.18 shows the percentage of all instantiations of the Alternating
pattern with p AL greater than an acceptance threshold that increases from
0 to 1. The other line is for the Windows experiments described in Section
8.3.3. We arbitrarily picked 0:9 as the acceptance threshold to select prop-
erties. The initial result had 490 properties, too many to inspect manually.
Next, the chaining method converted the properties to 17 chains. We applied
the chaining method before applying other heuristics because other heuristics
might prevent a long chain from being formed. Then we pruned the results
by applying the static call graph based heuristic, which reduced the number
of chains to the 15 chains shown in Table 8.3.

8.3.2.2 Comparison with JTA Specification

The longest chain (Figure 8.19) has 24 events including not only the public
methods declared in the JTA specification but also private methods internal to
the implementation of JBoss. After omitting the private methods, we obtain
the shorter chain shown in Figure 8.20. The TxManager and Transaction-
Impl classes implement the JTA TransactionManager and Transaction inter-
faces respectively. This chain is almost identical to the object interaction dia-
gram in the Java Transaction API (JTA) specification except that Perracotta
does not infer the alternating relationship between enlistResource and delistRe-
source . This is because whenever enlistResource is called, either delistResource or
commitResources must be called. Therefore, a resource does not have to be
delisted. As shown in Figure 8.20, Perracotta incorrectly infers enlistResource
! commitResources as it is the dominant behavior in the trace.
The longest chain reveals more than just how the public APIs interact.
It also provides insight into the internal implementation such as starting and
committing a transaction, which would help new developers understand JBoss.