Databases Reference
In-Depth Information
Bus waiting for trip 1
Passenger 0 gets in
Bus drives around Charlottesville
Passenger 0 gets off
Bus waiting for trip 2
Passenger 1 gets in
Bus drives around Charlottesville
Passenger 1 gets off
Bus stops for the day
FIGURE 8.25: Sample output of Bus Simulator with n = 2, C = 1, and
T = 2.
ing the inferred properties can increase users' condence that desirable tem-
poral properties are preserved by modifications. Furthermore, inconsistencies
among the inferred properties can reveal interesting facts such as bug fixes or
program enhancement.
This section presents experiments applying Perracotta to two families of
programs: student implementations of a multi-threaded programming assign-
ment in a graduate software systems course and archived versions of OpenSSL
[63]. Because all programs in each case implement the same informal speci-
fication, any differences in the inferred temporal properties are likely to be
interesting. For these experiments, we use the acceptance threshold of 1:0 for
all the properties, thus only consistently true properties are considered. We
use Perracotta to infer the strictest properties for each version of a program.
We call the inferred properties the signature of each version and compare the
signatures of program versions.
8.4.2.1
Tour Bus Simulator
The first experiment used submissions for an assignment in a graduate
software systems course taught at the University of Virginia in fall 2003. The
assignment was a multi-threaded program simulating the operation of city bus
with an informal specification, paraphrased below:
Write a program that takes three inputs: n, the number of passengers, C,
the maximum number of passengers the bus can hold (C must be n), and
T, the number of trips the bus takes, and simulates a tour bus transporting
passengers around town. The passengers repeatedly wait to take a tour of town
in the bus, which can hold a maximum of C passengers. The bus waits until
it has a full load of passengers, and then drives around town. After finishing
a trip, each passenger gets off the bus and wanders around before returning to
the bus for another trip. The bus makes up to T trips in a day and then stops.
The assignment also specified the format of input and output. Figure 8.25
shows the output of a typical execution when n = 2, C = 1, and T = 2.
Because the outputs corresponded to events of interest to us, we did not
Search WWH ::
Custom Search