What to Hand In

You should hand in:

• A description of the two formal models outlined above. Ideally this should be formatted and checked using Fuzz, but it need not be. As with all Z documents, the formalism should be accompanied by enough prose to explain what is going on. You may work in groups to produce this document.
• As individuals you should also turn in commentary addressing the following questions:
  1. What important aspects of the modeled architectures are (intentionally) left out of the model.
  2. One might imagine that an interesting property of a blackboard system would be whether the knowledge sources interfere with each other. For the blackboard system, do you think it would be possible to model some notion of ``non-interference?'' (You need not model it, but you should explain the reasoning behind your answer to this question.)
  3. For the spreadsheet system, is the Circular property defined in the events paper a relevant concept? Why or why not?
  4. For both the blackboard and spreadsheet models, explain briefly which of the other formal event models described in the paper is most similar.

We will make a copy of the Z description for the event system described in [GN91] available to you.