1.3 CSP Refinement

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].

Traces refinement

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.

Failures refinement

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.

Failures-Divergences refinement

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:

• Traces refinement is used for proving safety properties.
• Failures-divergence refinement is used for proving safety, liveness and combination properties, and also for establishing refinement and equality relations between systems.
• Failures refinement is normally used to prove failures-divergence refinement for processes that are already known to be divergence-free. It does have other uses, but these are somewhat more sophisticated. See the file ‘abp.csp’ in the FDR ‘demo’ directory for some discussion of this issue.

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

A formal system supporting refinement can be used in a number of ways:

• We can develop systems by a series of stepwise refinements, starting with a specification process and gradually refining it into an implementation. Since our notions of refinement are all preserved by the operators of CSP, there is no need to apply refinement rules only at the highest levels in this process. For example, if the parallel composition of P and Q refines a specification S, written

  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.

• The same observation about compositionality, or monotonicity, of refinement, means that it is always possible to replace any component of a system by one that refines it, and retain any correctness properties proved using the same notion of refinement.
• A proposed implementation can be compared to idealised processes representing specifications. These specifications might be complex and be intended to capture the complete behaviour of the implementation, or be simple and capture a single desirable property such as deadlock freedom.
• By proving failures-divergence refinement both ways, two processes can be shown to be equivalent and therefore interchangeable.

1.3.2 Simple buffer example

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).

1.3.3 Checking refinement

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.

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.