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

In summary, the inferred properties represent interesting temporal behav-
iors of Daisy. Several of the inferred properties such as DaisyDisk.readAllocBit !
DaisyLock.relb involve more than one class, which indicates delocalized plans
that would be useful to aid programmers in understanding the system.

8.3.2 JBoss Application Server
An application server (AS) is middleware that provides important services
such as transactions, security, and caching for running web applications [45].
A web application built upon an application server reuses these well-tested
services and components.
A Java application server is an application server that runs on a Java
virtual machine [45]. The J2EE specification defines the interface between a
web application and a Java application server [45]. JBoss is open-source and
is currently one of the most widely used Java application servers [47].
We are particularly interested in the APIs of the transaction management
service because a transaction occurs in multiple stages with certain temporal
ordering constraints. The Java Transaction API (JTA) specification defines
the interfaces between a transaction manager and the other participants in
a distributed transaction system: the application, the resource manager, and
the application server [49]. The JTA specification has an object interaction
diagram [31] as an illustration of how an application server may handle a
transactional connection request from an application (note that the diagram
is just one typical scenario, but not a specification) [49]. An application server
starts a transaction by first calling the begin method of the transaction man-
ager (TM). Next the AS tries to get a transactional resource from the resource
adapter (RA). The AS calls the enlistResource method to declare its ownership
of a resource. Then the application does its work. To finish a transaction, the
AS calls the delistResource method to release its ownership of the correspond-
ing resource and then commits the transaction. The transaction commission
follows a two-stage commit protocol that first prepares and then commits the
transaction.

8.3.2.1 Inference Results

We obtained the source code of the JBoss Application Server version 4.0.2
from www.jboss.org (the latest one at the time of our experiments). The source
code distribution included about 4000 fully automated regression test cases.
We used JRat to instrument all method invocations of the transaction manage-
ment module (i.e., all classes in the org.jboss.tm package) and ran the regression
test suite. After dropping events that occurred fewer than 10 times, the ex-
ecution trace contained 2.5 million events with 91 distinct events (we only
monitored the entrance events). Perracotta analyzed the trace in 80 seconds
on a machine with one 3GHz CPU, 1GB RAM, and Windows XP Professional.