Download Failures-Divergence Refinement

Chapter 1: Introduction
6
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 vFD is defined as
follows:
P vFD Q =
b 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, vFD is equivalent to vF .
As implied by the name of FDR, we consider vFD to be the most important of these three.
We will generally abbreviate vFD by v. 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.
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 v P k Q,
X
then we can develop the system further by refining P and Q separately: if P v P 0 and
Q v Q 0 , then the composition of P 0 and Q 0 will also refine S :
S v P 0 k Q 0,
X
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.