[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The notion of refinement is a particularly useful concept in many forms of engineering activity. If we can establish a relation between components of a system which captures the fact that one satisfies at least the same conditions as another, then we may replace a worse component by a better one without degrading the properties of the system. Obviously the notion of refinement must reflect the properties of a system which are important: in building bridges it may acceptable to replace a (weaker) aluminium rivet by a (stronger) iron one, but if weight is critical, say in an aircraft, this is not a valid refinement.
In describing reactive computer systems, CSP has been found to be a useful tool. Refinement relations can be defined for systems described in CSP in several ways, depending on the semantic model of the language which is used. In the untimed versions of CSP, three main forms of refinement are relevant, corresponding to the three models presented above. We briefly outline these below, for more information see [Roscoe97].
The coarsest commonly used relationship is based on the sequences of events which a process can perform (the traces of the process). A process Q is a traces refinement of another, P, if all the possible sequences of communications which Q can do are also possible for P. This relationship is written PQ.If we consider P to be a specification which determines possible safe states of a system, then we can think of PQas saying that Q is a safe implementation: no wrong events will be allowed.
PQ traces(Q)traces(P)
Traces refinement does not allow us to say anything about what will actually happen, however. The process STOP, which never performs any events, is a refinement of any process in this framework, and satisfies any safety specification.
A finer distinction between processes can be made by constraining the events which an implementation is permitted to block as well as those which it performs. A failure is a pair (s,X), where s is a trace of the process and X is a set of events the process can refuse to perform at that point (and, to add a little more terminology, X is called a refusal). Failures refinement is defined by insisting that the set of all failures of a refining process are included in those of the refined process.
PQ failures(Q)failures(P)
A state of a process is deadlocked if it can refuse to do every event, and STOP is the simplest deadlocked process. Deadlock is also commonly introduced when parallel processes do not succeed in synchronising on the same event.
The failures model does not allow us to easily detect one important class of states: those after which the process might livelock (i.e., perform an infinite sequence of internal actions) and so may never subsequently engage in a visible event. So, a semantic model more thorough (in this respect) than the failures model is desirable.
The failures-divergences model meets this requirement by adding the concept of divergences. The divergences of a process are the set of traces after which the process may livelock. This gives two major enhancements: we may analyse systems which have the potential to never perform another visible event and assert this does not occur in the situations being considered; and we may also use divergence in the specification to describe “don’t care” situations. The relation is defined as follows:
PQ failures(Q)failures(P) divergences(Q)divergences(P)
Formally, after a divergence we consider a process to be acting chaotically and able to do or refuse anything. This means that processes are considered to be identical after they have diverged.
Naturally, for divergence-free processes, which include the vast majority of practical systems, is equivalent to
As implied by the name of FDR, we consider to be the most important of these three. We will generally abbreviate by .The failures-divergence model, and its corresponding notion of refinement, are usually taken as the standard model of CSP.
All three of these forms of refinement are supported in FDR. We would normally expect them to be used in the following contexts:
The following sections illustrate how refinement might be used (by working through a simple example) and explain how the FDR tool can check refinement in an automated way.
1.3.1 Using refinement | ||
1.3.2 Simple buffer example | ||
1.3.3 Checking refinement |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
A formal system supporting refinement can be used in a number of ways:
S PQ
then we can develop the system further by refining P and Q separately: if PP'and QQ'then the composition of P’ and Q’ will also refine S:
S P'Q'
We do not need to check this condition explicitly.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
As a simple example, consider the specification that a process behaves like a one place buffer. This can be represented by the simple process COPY:
COPY left?x right!x COPY
A possible implementation might use separate sender and receiver processes, communication via a channel mid and an acknowledgement channel ack:
SEND left?x mid!x ack SEND
REC mid?x right!x ack REC
SYSTEM (SEND REC) \ X, where X={|mid,ack|}
In this system, the process SEND sends the messages it receives on left to the channel mid (which is made internal to the SYSTEM by the use of hiding) and then waits for an acknowledgement, ack. In a rather similar way, REC receives these messages on the internal channel and passes them on to right. It then performs the acknowledgement ack, allowing the whole process to start again.
We may show that COPYSYSTEMconfirming that the extra buffering introduced by having two communicating processes is eliminated by the use of an acknowledgement signal. In fact, SYSTEMCOPYis also true, so these two processes are actually equivalent. Other, weaker specifications that could be proved of either include
DF = a DF
which specifies that they are deadlock-free (this process may select any single event from the overall alphabet but can never get into a state where it can refuse all events).
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
For processes which can only mutually reach a finite number of distinct pairs of states, we may check that a refinement relation holds between them by a process of induction(1). The basic strategy is as follows: suppose we consider any corresponding states S of specification Q and I of implementation P. The conditions which any such pair must satisfy if failures-divergences refinement is to hold are that any event which is immediately possible for the implementation must be possible for the specification:(2)
a (I) (S)
Any refusal of I is allowable for S:
X (I refuses X) (S refuses X)
And divergence is only possible for I if it is for S:
I S
Because any subset of a set which can be refused is also a refusal, it is sufficient to test that each maximal refusal of I is included in a refusal of S.
Having checked that a particular pair is correct, it is then necessary to check that all pairs reachable from this one are, and so on. Refinement is established once all the pairs that are reachable have been checked (i.e., all the new states are ones that have already been seen).
In general, simply exploring the cross-product of the state-spaces in this way does not work: just because it is possible for the specification to reach a state which appears to exclude a given behaviour of the implementation, it is not necessarily the case that there is not another possible state of the specification machine which would permit it(3). In order to avoid this possibility, FDR requires — and ensures — that the specification process be reduced to a normal form, with at most one state reachable on any trace; in practice, this means that all internal transitions are eliminated and that there is at most one transition from any state by any given event. The algorithm to achieve this produces states in the normalised machine corresponding to sets of states in the unnormalised specification; in theory (and in some pathological cases) this may make the normal form exponentially larger than the original, but in most real examples normalisation in fact reduces the state-space, often dramatically.
FDR is designed to mechanise the process of carrying out refinement checks. For a wide class of CSP processes, it is possible to expand the state space of the process mechanically, and perform the tests above using a standard search strategy.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] |
This document was generated by Phil Armstrong on November 17, 2010 using texi2html 1.82.