Simple State-Based Refinement

Abstract

One central distinction in formal methods is between those based on state, and those based on behaviour. In most applications it is essential or at least practical to have both. State based systems need behavioural elements in order to consider aspects of interaction with an environment, for example to record which changes of state are due to the system’s ongoing execution and which are in response to an externally provided stimulus. Behaviour based systems can use state and data for abstraction, for example recording the number of free spaces as a number instead of a behaviour that encodes directly how many allocation operations will still succeed. The rich research field of “integrated formal methods” considers formalisms that have both, through extensions or integration of different formalisms. We will return in detail to these issues in Chap. 9 and on. The models we have looked at so far concentrate on behaviour, and states are fully characterised by the behaviour that will be possible from that point on. Observing only the (possible) behaviour tells us everything there is to know in a LTS. In this chapter we will look at a different class of elementary models that take the complementary view. What we will be observing is states rather than behaviours; and behaviour will be implicit, in the sense that we have to draw the conclusion that “something must have happened” if we can observe that the state has changed. We observe what “is”, not directly what “happens”.