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

TABLE 8.7: Bus Simulator Properties

P S Property in Correct Versions Property in Faulty Version

wait drives Alternating MultiEffect

wait gets off MultiEffect CauseFirst

drives gets off MultiEffect CauseFirst

wait gets in MultiEffect MultiEffect

gets in drives MultiCause MultiCause

gets in gets off CauseFirst CauseFirst

drives stops MultiCause N/A

gets in stops MultiCause N/A

wait stops MultiCause N/A

gets off stops MultiCause N/A

need to instrument the programs. Instead, we mapped the output logs directly
to event sequences. In the mapping, we considered these five events:

1 wait (Bus waiting for trip n)

2 drives (Bus drives around Charlottesville)

3 stops (Bus stops for the day )

4 gets in (A passenger gets in)

5 gets o (A passenger gets o )

Note that the numbers of the trip and passenger were ignored in our event
mapping to reduce the number of distinct events.
A correct solution must satisfy several temporal properties:

(a) The bus always drives with exactly C passengers.

(b) No passenger jumps off or on the bus while it is running.

(c) No passenger starts another trip before getting off the bus.

(d) All passengers get off the bus before passengers for the next trip begin
getting on.

We analyzed eight different submissions, all of which were previously eval-
uated as correct by a grader.
Inference Results. We executed each solution 100 times with randomly
generated parameters (20 C 40, C + 1 n 2C, and 1 T 10).
We used Perracotta to infer the strictest pattern the execution traces satisfy
(Section 8.2.4.1). Perracotta inferred the same set of temporal properties for
seven out of the eight submissions. Table 8.7 summarizes the results.
Perracotta inferred the Alternating pattern, wait ! drives , for seven of the
programs. In the other program, the strictest pattern inferred for wait and