CMU 15-671Models of Software SystemsFall 1995
Reasoning About State Machines
Garlan & Wing Handout 6 25 September 1995
Given a state machine model of a system, we can do some formal reasoning about properties of the model. It's important to remember that we are proving some property about the model of the system, not the system itself. If the model is ``incorrect'' then we may not be able to prove anything useful about the system. Worse, if the model is ``incorrect'' then we may be able to prove something that has no correspondence to the real system. However, we hope that we've modeled our system properly so that whatever we prove about our model is true of the system being modeled.
But then, why not just reason about the system itself directly? One reason is that it's often impossible to reason about the system itself because it's too large, too complex, or too unwieldy. Another is that we may be interested in one aspect of the system and want to abstract from the irrelevant aspects. Another is that we may not actually have a real system; our model could simply be a high-level design of a system we might build and we want to do some reasoning about our design before spending the dollars building the real thing. Another is that it may be impossible to get our hands on the system (maybe it's proprietary). Another is that it may be impossible for us to run the system to check for the property because of its safety-critical side-effects (like setting off a bomb). So, in some cases, the best we can do is reason about a model of the system, and not the system itself.
In this handout I'll discuss a few kinds of properties we might
want to reason about a state machine model.
The most important
of these is invariant properties, properties that are
true of every reachable state in the system.