Databases Reference
In-Depth Information
properties including program verification (Section 8.4.1) and program differ-
encing (Section 8.4.2).
Complex systems are hard to understand in that it is challenging to recog-
nize delocalized plans [55]. Delocalized plans are \programming plans realized
by lines scattered in dierent parts of the program." [55] We hypothesize that
our dynamic temporal specification inference technique can effectively detect
certain delocalized plans.
To test the hypothesis and also evaluate the scalability, accuracy, and
cost of our technique, we conducted several case studies on a wide range of
programs:
(a) Bus Simulator, a collection of student submissions for an assignment of
implementing a multi-threaded C program in a graduate course taught
at the University of Virginia.
(b) Daisy, a prototype implementation of a Unix-like file system in Java.
Daisy was developed as a common testbed for different program verifi-
cation tools [18].
(c) OpenSSL, a C implementation of the Secure Sockets Layer (SSL) speci-
fication [63, 74]. Our experiment focuses on its handshake protocol.
(d) JBoss, a Java application server conforming to the J2EE specification
[45,47]. Our experiment focuses on its transaction management module.
(e) Microsoft Windows kernel APIs, a set of about 1800 functions written in
C or C++. These functions are the foundation of the Windows operating
system. Our experiment is on Windows Vista.
Table 8.2 summarizes the characteristics of these five testbeds. Bus Sim-
ulator and Daisy are small prototype programs. They are good for proof-of-
concept experiments. The other three programs are complex and widely used.
They are valuable for understanding the strength and weakness of our tech-
nique when it is applied to real systems. Our testbeds differ in the quality
of specication available. The Bus Simulator comes with instructor's English
description of a list of properties a valid implementation ought to have. Daisy
does not have any temporal specification except a list of properties in English
provided by one of its developers. OpenSSL has an extensive specification, the
SSL specification [63, 74]. The SSL specification includes a detailed descrip-
tion as well as a finite state automaton of the handshake protocol. The JBoss
application server implements the J2EE specification [45, 47]. In particular,
its transaction management module implements the Java Transaction API
(JTA) specification [49], which has an extensive English description and an
object interaction diagram illustrating the temporal behavior of the compo-
nents participating in a transaction. For the Windows kernel APIs, some of
their temporal rules are documented either publicly in the MSDN library or
privately in some internal documents. These documented rules are, however,
Search WWH ::
Custom Search