CISC422/853: Formal Methods in Software Engineering: Computer-Aided Verification (Winter 2009)

• Either you install it yourself:
  • Go to the Bogor webpage
  • Download Bogor code (must accept licence agreement and create new account)
  • Install Bogor (follow instructions)
• Or, you use the installation on the caslab machines
  • Start Eclipse and then follow instructions on "Running Bogor"

• store the position of the farmer and the items in variables,
• initialize these variables appropriately and then start a thread that implements the moves of puzzle,
• use the invisible tag whenever appropriate to prevent unnecessary/illegal interleavings from being considered,
• use assume(b) to prevent illegal positions (e.g., wolf can eat goat) from being considered. assume(b) evaluates the expression b in the current state. If b evaluates to true, assume(b) has no effect and execution proceeds as normal. If b evaluates to false, the search at the current state is stopped and the searcher backtracks to an earlier state in the computation tree (if it exists). In other words, if b is false in state s, execution of assume(b) in s will remove the entire computation subtree rooted at s from the analysis.

• express the final position of the puzzle (everybody is on the other side) as an assertion A
• use the technique discussed in class to show that the negation of A is not an invariant, that is, that it is not the case that the system never reaches the final position

• Initial position: Farmer 1 and his boat and all items are on shore 1. Farmer 2 and his boat are on Shore 2.
• Final position: Farmer 1 on Shore 1 and Farmer 2 and all items on Shore 3.
• Moves: As before, each farmer can carry at most one item in his boat. Farmer 1 can only cross River 1, while Farmer 2 can only cross River 2. In other words, Farmer 1 will always be either on shore 1 or Shore 2 and Farmer 2 will always be either on Shore 2 or Shore 3.
• Illegal positions: As before, neither the wolf and the goat, nor the goat and the cabbage must be alone (i.e., without a farmer) on any of the 3 shores.

• start up two threads (one for each farmer) to implement the moves of the puzzle,
• use invisible and assume as appropriate.

Let n be the number of workers.
Rule 1. Every worker starts with rank r=0.
Rule 2. Every worker with rank r=0 can promote herself to rank r=1.
Rule 3. To promote herself from rank r to rank r+1 an worker shall:
        a) first, record herself as having rank r+1, and then
        b) record herself as the last worker to have reached rank r+1.
Rule 4. Every worker in ranks 0<r<n can promote herself to rank r+1 iff
        a) she is not last worker to have reached rank r, or
        b) all other workers have ranks below hers.
Rule 5. Workers with rank n are boss; after a finite amount of time 
        they have to demote themselves back to rank 0.

• Single-Boss property: "At any given time, there is never more than one boss!"

• Part a): To determine if the property above always holds, they have written a concurrent Java program to simulate the rules. Download the code [SleeplessCode.java, Timer.java], run it (it requires Java 1.5, aka Java 2) and understand how it works. Briefly explain why the simulation is insufficient to determine if the property always holds no matter how long the simulation is run.
• Part b): Using the Java code as a guideline, implement the promotion rules given above in BIR:
  • Implement each worker as a concurrent process
  • Each worker process should be executing in an infinite loop
  • Use two array variables that are shared among the worker processes to keep track of
    • the rank that each worker currently has
    • for each rank, the worker (if any) who was the last to have been promoted to that rank
  • Give the cooperative 3 workers, but make sure that your code can easily be changed to handle different numbers
  • Ignore the timing code in the Java program; Bogor doesn't support that.
  • To ease the coding effort in BIR, you may want to use the following BIR function isHighestProcess.bir. Place this function into your BIR system definition on the same level as your thread definitions. You can invoke the function from inside a thread using, e.g.,

    thread P(int id) {
      boolean isHighest;
      ...
      loc loc4:
    	isHighest := invoke isHighestProcess(id)
    	goto loc5;
      loc loc5:
    	when isHighest do { // process id can advance
    	...
      }
    		  

• Part c): Use Bogor to determine if the Single-Boss property holds in your BIR implementation with 3 workers.
• Part d): Use Bogor to convince yourself that in your code it is possible for at least one of the workers to become boss; in other words, that it is not the case that along all executions none of the workers ever becomes boss.
• Part e): Worker Smarty Pants suggests to replace Rule 3 above by:

  Rule 3. To promote herself from rank r to rank r+1 an worker shall:
          a) first, record herself as the last worker to have reached rank r+1, and then
  	b) record herself as having rank r+1.
  	    

  That is, the new Rule 3 is just like the old one except that the order of the steps a) and b) is reversed. Modify your BIR code from Parts a)-d) appropriately to reflect this replacement. Rerun your analyses. How does this modification affect the Single-Boss property?

• Part a): Brief explanation
• Parts b), c), and d): Listing of your BIR code (together w/ electronic submission by email (see below)) and "yes/no" answers for Parts c) and d)
• Part e): "yes/no" answer together with brief, intuitive explanation why proproty still holds (if your answer is "yes"), or counter example showing violation (if your answer is "no").

• BIR programs have names that clearly indicate which question and part they belong to
• you mention "CISC422/853" in the subject line
• the names of all students in the group (up to 2) appear

• correctness (your programs should correctly implement the moves of the puzzles or protocol; the BIR constructs should be used appropriately)
• readability (your programs should be as easy to understand and follow as possible)