Entering a specification using the Bandera User Interface

Now we are ready to create a new session and to check whether the property we specified above holds for this program. When creating a new session, we have the choice of creating a new session file or adding the session to the existing session file. Let's add a new session to the existing session file.

• Click on the Open option on the main frame top tool-bar. This will bring out the Session Manager window and display the current sessions. At this point you can click on the New option on the left of the window. This will enable the rest of the options such as Activate and Remove. Your session is called Untitled1 by default. You can rename it by positioning the cursor in the Name field and typing the name you like as if you were working with a text editor. For simplicity, let's call this session MyPipeInt. Before you can proceed, you need to Activate this session.
• Now you need to specify the file that you want Bandera to work with. At the top of the Session Manager window you will see the following tabs: Sessions, Compiler, Property, Abtraction, Birc, Checker, and Misc. Click on the Compiler option. You should see that Bandera automatically chooses the classpath to be set to the directory where you invoked Bandera. If you followed the instructions above, you should have all your examples in the same directory (this is done for simplicity in this tutorial presentation, you don't necessarily need to have your files in the same directory). To specify the name of the file, click on the Edit option in the Source row. This will pop up another window that will list all of the JAVA source code files in the current directory. If you wanted to point to a file in another directory, you would simply navigate through the hierarchy of directories using the options at the top of the window. Left-click on PipeInt.java, then click on the Select option at the bottom of the window. You are done with choosing the file.
• If the specification that you want to check has been been entered into Bandera before or if you have written it manually using a text editor, you can choose the Property tab at the top of the Session Manager window and point to the existing specification file for the specification. However, for this example, we will create the specification file holding the specification to be checked from scratch using the BUI Property Manager. The BUI Property Manager provides a set of pull-down menus that allow you to insert declared predicates into specification patterns.

  Note: In order to build the database of declared predicates, Bandera first needs to load the .java source files containing the declared prediates. This will cause the predicates to be parsed and type-checked.

  Accordingly, close the Session Manager window by clicking on OK at the bottom. If you look at the top tool-bar of the main frame, you should see that only JJJC option is enabled. To load the source file, click on the RUN option. You are now ready to use the BUI Property Manager to create a specification to be checked.

• Find the Property option on the tool-bar of the main frame and click on it. This will bring out the Property Manager window. You will see three tabs at the top of the window: Property, Temporal Logic, and Assertion. Choose Temporal Logic tab. At this point there is only one option enabled, you can only Add a new formula. Click on Add. By default the name of the formula is Untitled1. After activating the property by clicking on the Activate/Deactivate you can rename it by editing the Name field of the window. Let's call this property stage1ShutdownProp.
• Now move your attention to the bottom part of the Property Manager window. Before we proceed to the picking of the predicates, we will edit the Quantifications field. One of the predicates we want to use in the formula appears in the run method of thread Stage1. We need to quantify this predicate for all instances of Stage1, therefore, enter the following line in the Quantifications field:

     forall[s:Stage1].

  The property we want to check is a response property with a global scope, so under the Pattern Name choose Response. Under the Pattern Scope choose Globally.
• Now we are ready to pick the predicates. We will start with the first proposition of the formula, so under Proposition choose P and right-click in the field on the right. You should see the Add a predicate window pop up. Left-click on this little window. It will bring out another window that will let you choose the predicate for P. You should see a picture in front of you as shown in Figure 11.

   

   

  
  Figure 11: Property Manager Window
  

  Choose PipeInt.main.c1StopCall out of the list of predicates. Now you need to specify S. Follow the same steps as for P, only choose Stage1.run.stage1Shutdown predicate out of the list of predicates. Once this predicate name appears in the text box, add (s) at the end of the predicate name to reflect that we are working with a predicate for all instances of Stage1. After you are done with defining S, the field you edited should look like:

     Stage1.run.stage1Shutdown(s)

  It is always a good idea to click on Expand option to check whether your formula is valid. Go ahead and expand the formula, it should be valid.

• You can save the property you generated into the file. Click on the Property tab at the top of the Property Manager window and choose Save as option at the bottom. You can save the file in any directory under any name you like, but you must give your specification file the extention .specification. You can close the Property Manager window now by clicking on OK option at the bottom.