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

In summary, Perracotta successfully infers a complex finite state machine
that is consistent with the JTA specification. This demonstrates that Perra-
cotta can help programmers understand a real legacy system. Suppose there
is no specification available for the transaction management module; it would
have been a great challenge for programmers to discover its temporal behav-
iors by hand because these properties cross the boundary of many modules
and represent a non-trivial delocalized plan. These properties would also be
dicult for static analysis to infer because JBoss extensively uses polymor-
phic interfaces, pointers, and exception handlers. Precisely handling all these
features is still beyond the state-of-the-art of static analysis. In addition, the
static call graph based heuristic and the chaining method are helpful for reduc-
ing the number of properties and presenting the results. On the other hand,
the naming similarity based heuristic is not very useful in the experiment since
being a Java program, JBoss has few methods that implement basic resource
management and locking disciplines.

8.3.3 Windows
In this experiment, we applied Perracotta to infer API rules for the latest
(as of summer 2005) kernel (ntoskrnl.exe) and core components (hal.dll and
ntdll.dll ) of Windows Vista. Perracotta not only inferred many documented
properties, but also found several important but undocumented properties.
We checked 10 arbitrarily selected properties using the ESP verifier, which
found a serious deadlock bug in the NTFS file system (see Section 8.4.1.2).

8.3.3.1 Inference Results

We obtained 17 execution traces from a developer in the Windows core
development team. This developer instrumented APIs of the Windows kernel
and core components and collected these traces by running some typical Win-
dows applications (e.g., Windows MediaPlayer, Windows MovieMaker). He
collected these traces mainly for performance tuning and debugging. We did
not have any control of generating execution traces because these traces had
already been generated before we started our experiments. In particular, the
execution traces included the thread context information, but did not include
the values of function arguments.
The lengths of the traces ranged from about 300,000 to 750,000 events,
for about 5.8 million total events. The number of distinct events in each trace
varied from around 30 to 1300. On average, each execution trace had about
500 distinct events. Perracotta analyzed all traces in 14 minutes on a machine
running Windows XP Professional with one 3GHz CPU and 1GB RAM. As
with JBoss, we set the acceptance threshold for p AL to 0:90. Perracotta in-
ferred 7611 properties, too many to manually inspect. We randomly selected
200 inferred properties and found that only 2 of them are interesting. So we
applied the call graph and naming similarity heuristics to select the interesting