CMU 15-671Models of Software SystemsFall 1995
Relating State Machines: Satisfies
Garlan & Wing Handout 9 9 October 1995

This handout discusses the problem of whether one machine satisfies (in some sense) another. It should be read simultaneously (if that's possible!) with Handouts 10 and 11, which give specific examples.

Just as there is not one standard notion of equivalence, there is not one standard notion of ``satisfies.'' In this handout we give a definition that is reasonable, representative, and used in practice.

There are three key ideas that this handout presents.

• A definition of satisfies in terms of a subset relationship between behavior sets of two machines.
• The notion of a mapping, called an abstraction function, that relates states of one machine to states of another.
• A proof technique that uses the abstraction function in a ``commuting'' diagram (see Section 3.1) to relate state transitions of one machine to state transitions of another.

Although our notion of satisfies and the proof technique that I present here may seem specific to the model of state machines that I have described so far, what's the most important idea for you to learn from these handouts is the notion of an abstraction function. You will also see it again, in a different guise, when we cover refinement in Z.

• Why Would You Care About ``Satisfies''?
• What Does Satisfies Mean?
  • Binary Relations
  • State Machines
• Showing One Machine Satisfies Another
  • A Proof Technique
  • Rationale
  • Abstraction Functions and Representation Invariants
  • Variations on a Theme
• About this document ...