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

Files, Directories
Inodes, Blocks, Allocation Bits
Byte Streams
Hard Drive
FIGURE 8.17: Daisy's System Architecture. Daisy emulates the hard drive
through a Java RandomAccessFile object.
by no means complete as our experiment discovered many undocumented im-
portant rules. We include two systems with extensive specifications (OpenSSL
and JBoss) so that we can compare the inferred properties against the existing
specifications. These existing specifications serve as a guideline of what prop-
erties are important and interesting, without which it would be much more
dicult to tell whether the inference approach produces useful results.
Next, Sections 8.3.1 to 8.3.3 present the inference results for all the testbeds
except OpenSSL and Bus Simulator. We defer the presentation of the exper-
iments on OpenSSL and Bus Simulator to Section 8.4.2 because the focus
of these experiments is on evaluating the usefulness of the inferred proper-
ties in program differencing. Our experimental results strongly support that
Perracotta can be useful for program understanding. Perracotta discovered
interesting temporal properties for all the testbeds. For the Windows kernel,
Perracotta inferred 56 interesting properties, many of which were undocu-
mented. For JBoss, Perracotta inferred a 24-event finite state machine that
was consistent with the JTA specification. Many of the JBoss properties rep-
resent delocalized plans as the events cross multiple \distant" modules of the
target systems. Discovering these delocalized plans is valuable because they
can be hard to discover by manual inspection and violating them when mod-
ifying the system could introduce serious errors.
8.3.1 Daisy
Daisy is a prototype Unix-like file system implemented in 2000 lines of
Java code [18]. Daisy's architecture has four layers as shown in Figure 8.17.
At the bottom, Daisy emulates the hard drive using a RandomAccessFile ( RAF )
object. Above it, the disk layer abstracts the hard drive into byte streams.
The next layer abstracts the byte streams into blocks. The top layer provides
an interface for files and directories.
We used JRat to monitor the invocation of all Daisy methods except
those inherited from the Object class (e.g., toString ). We created a wrapper
for the Java RandomAccessFile class so that JRat can monitor its methods.
JRat recorded a method's signature, thread, this object, and arguments.
To execute Daisy, we adapted the test harness in the Daisy distribution.