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

For this assignment you will consider a system of threads that are intended to model the behaviour of three chameleons who have stayed too long at a boring cocktail party.

Consider three chameleons placed in a triangle configuration, that is, each one can comunicate with either one of its neighbours. Below is a graphical representation:

These chameleons can assume the colors red, green or blue. Being bored at the cocktail party, they make no effort at polite conversation with others but instead simply change colours according to the following rule:

The final goal of these chameleons is to be all of the same colour. When such a situation is reached, the chameleons leave the party. There is a catch, however. Each chameleon cannot see one of the other two because his view is blocked by a large obnoxious dragon. This means that each chameleon can only exchange colour information with one of its neighbours at a time. For instance, in one "communication round", a chameleon may send its own colour to its left neighbour and receive the left neighbour's colour in response. Based on that information alone (i.e., without interacting with the third chameleon), a decision to change colour is made. Fortunately, a hyperactive frog is also attending the party who he is constantly hopping around the dragon. To check if the other two chameleons match his/her color, a chameleon may ask the frog about the current situation. The frog replies with a value of 'true' if all the chameleons have the same color and 'false' otherwise.

Write a Promela specification of the chameleons problem where the frog and each chameleon are modeled as a separate thread (i.e., process). This will involve designing a correct (error free) communication protocol between chameleons that allows them to exhange color information and guarantee that a pair of chameleons can both complete a color switch together without one of them leaving to negotiate a switch with the third chameleon. Moreover, your protocol must ensure, once they are all the same color, that the chameleons eventually stop asking each other to change colors and that they all leave the party.

To get you started, here is a fragment of a model followed by some comments on how to arrive at a completed solution.

1. [23 points] Give a concise but convincing description of the outline of your protocol. Explain the following points clearly.
   • How does your protocol ensure that two chameleons can exchange color information and switch colors without interruption from another chameleon? Does it work for all initial states? Why/why not?
   • How is the communication with the frog handled, including proper locking of the color array as explained below, and how is the behavior of the frog modeled?
   • How does your protocol arrange for the chameleons to leave the party together, e.g., without leaving one chameleon alone standing asking his neighbor for color information (and thus deadlocked)? How does it guarantee that IF all the chameleons are the same color THEN eventually they will leave the party?
   • Why is your protocol deadlock free?
   The 23 points for this task will be awarded based on the quality of your code and your answers.
2. [3 points] Use Spin to verify that your model is deadlock free. What command line options or XSpin verification parameters did you use?
3. [5 points] Consider the requirement: "All chameleons will eventually leave the party".
   • Is this a safety or liveness property?
   • Describe how you use the Spin to check for this requirement.
   • Does this requirement hold or fail for the system (why or why not)?
4. [7 points] Use Spin to verify that it is possible for the chameleons to leave the party. Note that this is essentially an existential path property: "there exists a path through the system where the chameleons leave the party". How can you check this requirement in LTL-based Spin, since LTL only allows one to express universal path properties?
5. [5 points] Use Spin to verify the following requirement: "If the system ever arrives at state where all the chameleons have the same color, then all the chameleons will eventually leave the party". Describe how you render the requirement for Spin verification.
6. [7 points] Use Spin to verify the following invariant: "If the chameleons leave the party, they all possess the same non-black color". This requirement can be formalized in LTL and as an assertion. Describe both ways of rendering the requirement for Spin verification (remember the assertion must appropriately capture an invariant, i.e., it must guarantee that the property holds at every possible execution state for the chameleon and frog threads).

• Your final Promela model as a paper copy.
• Also send that same model in an email (plain text please) to the TA Scott. You will receive no credit if your Promela model cannot be compiled and run in Spin.
• Following your Promela model, text that answers the questions above.

1. Note that the missing parts in the provided protocol skeleton should be filled without the use of the Promela statements atomic and timeout.
2. After an analysis, Spin tells you which parts of your Promela code were "unreached"; use that to avoid unreached code in your solution as much as possible.
3. The three main design issues are
   • (a) how to have each chameleon communicate with its neighbors about changing colors in a dead-lock free manner
   • (b) how to detect that all chameleons have the same color and then have each chameleon transition to the 'leave_party' state without leaving other chameleons behind waiting for a communication from a neighbor.
   • (c) using the provided lock mechanism to guarantee that the frog does not see unstable intermediate states associated with two chameleons changing color.
   For (a), the skeleton solution above specifies that communication between chameleons is via rendezvous channels. One way to ensuring that communication is deadlock free is to have a chameleon interact differently with its left and right neighors. For example, it might always listen for a message from the left (never initiating a message to the left) but always initiate messages to the right.

   You may find (b) to be the most difficult issue. The frog will tell you when everybody is the same color. Note, that following the rules of the game, if every chameleon has the same color, it is impossible for them to become different colors again -- use this fact to your advantage. The challenge is to get each chameleon to recognize that they are all the same color so that they avoid asking their neighbors for color information. Once everyone knows that they shouldn't ask neighhors for color information, then everyone can leave without worrying about having a chameleon deadlock due to an unanswered request.

   The problem with (c) is that each chameleon changes its own color, e.g., by assigning to 'color[id]'. Note that for each color change, TWO chameleons must change colors. You don't want the frog to observe the system after only one chameleon has changed color. Therefore, we will impose a locking mechanism to ensure exclusive access to the 'color' array. The frog should acquire the lock before the observing the system, and the chameleons that decide to change colors should acquire the lock before they change, then they both change colors, then the lock is released. Note that only one chameleon needs to acquire the lock, so you will probably want to have some convention where one of the two chameleons grabs the lock, then notifies the other that it OK to change colors. Once the other chameleon has changed colors, it then notifies the first chameleon that it is done, and then it is OK for the first chameleon to release the lock.

   Make sure you don't overlook (c). Overlooking (c) allows a situation where the chameleons leave the party without all the colors being the same.