The code to be checked in this example implements a pipeline of
threads where each stage in the pipeline processes inflowing data and then
passes the transformed data onto the next downstream stage.
Figure 8 shows the basic structure of the
pipeline system whose code is contained in the file
PipeInt.java
in the tutorial examples directory.
Figure 8 shows that the pipeline has three processing stages
(threads) followed by a ``listener'' thread that simply receives the
incoming data and prints it to the screen. The data fed into
the beginning of the pipeline is generated in the main method
of the PipeInt class. The threads in the pipeline are connected
by instances of a Connector class. For this example, a
connector is a simple queue that can hold up to one integer.
Let's look at the actual code in
PipeInt.java
beginning with the main method of class PipeInt. After
the instances of all four threads (Stage1, Stage2,
Stage3, and Listener) and connectors are created, a
for loop places integers from 1 to 100 into the queue of
the first connector c1 by calling c1's add
method. Following the for loop, c1's stop method
is called. Examing the code for the Connector class shows that
this causes a 0 to be placed into the queue of
c1. Each of the stage threads considers an incoming 0
value to be a shutdown signal. Thus, if Stage number i
receives a 0 value from its upstream connector, it
(a) issues a stop on its downstream connector which causes
a 0 value to be placed in downstream connector's queue,
and (b) completes (i.e., shuts down). If Stage number i
receives a non-zero integer from its upstream connector from a call to
take on Connector number i, it grabs the integer,
increments it by 1, and puts it into the queue of the
Connector number i+1 via a call to the add method of
Connector number i+1. The Listener thread simply
takes the integers out of the last Connector's queue,
and when it receives a 0, the Listener shuts down.
Let's now consider how to use Bandera to see if the system satisfies a simple temporal property. In general, the methodology for rendering temporal properties in Bandera proceeds as outlined in Figure 5.5.1.
Figure 9: Methodology of property specification supported by Bandera
