Writing a specification using the Bandera Specification Language

In the implementation of Pipeline system, a useful requirement would be that if the main method of the PipeInt class is done (i.e., issues a stop to its down-stream connector), then each of the remaining stages in the pipeline shuts down. Let's concentrate on formalizing and checking this requirement for the first stage: if the main method of the PipeInt issues a stop on its down-stream connector c1, then Stage1 will eventually shutdown. The source code features mentioned in this requirement are the control point associated with the call to the stop method of c1 and the control point associated with the printing of the shutdown message in the run method of Stage1. We can use Bandera's LOCATION observable form to define predicates that become true when control reaches these points. To declare the observable control point in PipeInt's main method, we will (a) introduce a Java label (e.g., c1StopCallLoc) at the line of the control point (i.e., the line where Heap.c1.stop() appears), and (b) give the following Javadoc comment immediately above the method declaration.

  /**
   * @observable
   *   LOCATION[c1StopCallLoc] c1StopCall;
   */

Similarly, to declare the observable control point in Stage1's run method, you would (a) introduce a Java label (e.g., stage1ShutdownLoc) at the line of the control point (i.e., the line where System.out.println("Stage1 shutdown") appears, and (b) give the following Javadoc comment immediately above the method declaration.

  /**
   * @observable
   *   LOCATION[stage1ShutdownLoc] stage1Shutdown;
   */

Now that we have identified the relevant control points (one can also think of the execution of these control points as observable events) and declared predicates that hold true when execution reaches these control points, we are ready to state the temporal relationship between these events using Bandera's temporal specification pattern system. Note the example requirement has the following form:

if P occurs then eventually Q occurs

where P corresponds to the predicate PipeInt.main.c1StopCall and Q corresponds to the predicate Stage1.run.stage1Shutdown. In Bandera's pattern system, temporal properties that have this form are called response properties -- because Q must respond to P. Each pattern use must include a scope specification which delineates the segments of the execution trace where the property should hold. The example requirement should hold throughout the entire execution so it is said to have global scope. The actual rendering of the requirement in BSL is as follows.

     Response:  forall [s:Stage1].
                {Stage1.run.stage1Shutdown(s)}
                  responds to {PipeInt.main.c1StopCall} globally

Let's look at several aspects of this specification.

• The responds to identifies the property as instance of the response pattern instantiated with propositions Stage1.run.stage1Shutdown and PipeInt.main.c1StopCall.
• The globally specifies a global scope for the property (i.e., the property should be checked along the entire execution).
• The forall [s:Stage1] uses BSL's support for a form of object quantification that allows the property above to be stated for all instances s of the Stage1.
• Each predicates in BSL can be classified as either a static or an instance predicate. Static predicates are used to refer to static fields or program points of static Java methods; instance predicates are used to reason about instance fields or program points of nonstatic Java methods. The predicate Stage1.run.stage1Shutdown is an instance predicate because it refers to a location in the non-static method run of class Stage1. The predicate PipeInt.main.c1StopCall is a static predicate because it refers to a location in the static method main of class PipeInt. For instance predicates we need to specify the instance to which the predicate refers. In our case, the property holds for any instance of Stage1. Thus, the quantified variable s is supplied as a predicate to stage1Shutdown. In general, any time an instance prediate refering to an attribute of a class C is used in a BSL specification, the specification must include quantification over instances of C, and the quantified variable must be passed as a parameter to the instance predicate. Currently, BSL supports multiple universal quantifications at the outermost level. Existential quantification is not supported.

When processing this specification for Spin, Bandera will compile the response property above down to an LTL property of the following form

     [](P -> <>S)

where P is replaced with a lower-level predicates on internal representations that hold true at event of calling Heap.c1.stop() (similarly for S). The compiled formula for Spin also includes some additional structure needed to properly implement the quantification. Section 6 gives additional information about the syntax, semantics, and implementation of BSL specifications and object quantification.