CMU MSE 15-671, Models of Software Systems, Fall 1995
More on Z
Garlan & Wing, Homework 7 (really!), October 11, 1995
- 1. The following questions refer to the Birthday Book example. Suppose we would like to produce a follow-on product to the Birthday Book that is a bit more secure. In particular, it comes with a built-in password. If you know the password then you are allowed to change the entries in the book. Otherwise you are allowed to read the information, but not modify it.
- A. Define a new given type PASSWORD, a new enumerated type STATUS (say, OK, or NOTOK), and a global (axiomatic) function CheckPassword which returns a STATUS when applied to a given PASSWORD. You need not define what this function does -- just provide its signature so that it can be used in the rest of the specification.
- B. Using those definitions and the schema calculus operators augment the BirthdayBook state space so it contains a new field: authenticated which has type status (OK or NOTOK). (Note you should not need to substantially rewrite the original state space, but use schema operations to augment it.) Define an initial state schema for this new state space.
- C. Define a new operation Login, which sets the value of authenticated based on what CheckPassword returns.
- D. Augment the old operations so that they take into account this new field. (Again, you should use the schema calculus to do this.) Your new operations need not be robust, although you may feel free to make them so. (To do this you will have to modify the original set of reports to report an error if the user is not authenticated.)
- 2. The following quesitons refer to the Oscilloscope example.
- A. Suppose you wanted to produduce a specification of a three-channel oscilloscope (as compared to the two-channel version presented in the paper). What changes would you have to make to the original specification?
- B. Suppose you were asked to write a specification for an "invert" operation that could be "plugged in" to the signal processing stream. It should work on signals, and should reverse the sign of the signal values. Further more it should be able to be turned off and on. (E.g., if a signal has value v at time t, then the inverted signal will have value -v at time t.) Write the definition of this component. (You need not integrate it into the rest of the spec -- e.g., by modifying "ChannelParameters" etc.)