Download Compositional Verification of a Network of CSP Processes: using

20
J.Burton
a failure of the transformed process). Since we may work in the stable failures model, we are able to use
the process DIV, the immediately diverging process, to obscure failures in which we are not interested
without adding behaviours to the resulting process. We are able to do this in the following way.
Let P be a process expression. Then φ(P 2 DIV) = {(t, R) ∈ φP | t 6= h i}. That this is the case
follows from the definition of 2 in the stable failures model and the fact that the meaning of DIV in
this model is ({h i}, ∅) (the alphabet component is omitted here). In particular, we are able to obscure
failures derived from states where behaviour is complete over the channel set Bi , since condition LC
places no restriction on what may be refused in those situations. This aproach of working in the stable
failures model and (crucially) using DIV is also used in the checking of condition RE.
The following process, PROCi , is such that after any trace we may non-deterministically arrive at
b but which does not contribute to a failure of PROCi due to the
a state which offers all events in αQ
appearance of DIV in that state. Alternatively, we may arrive at a state which offers all events in αBi
and then takes us to a state that is simply immediately divergent whichever event from αBi we follow.
PROCi , ((2a∈αQb a → PROCi ) 2 DIV) u (2a∈αBi a → DIV).
b in parallel with PROCi , with the result that, for every failure (t, R) ∈ φQ,
b the
We then compose Q
b \ αBi added to it. This means that the refusal R ∩ αBi will survive the hiding of the
refusal R has αQ
b
events in αQ \ αBi . This gives us the following process:
b i , (Q
b k PROCi ) \ (αQ
b \ αBi ).
Q
b rather than simply φQ.
b This means
Note in part (2) of the following lemma that (w, X) ∈ φ⊥ Q,
b
that we can look at the meaning of the process expression Q in the stable failures model rather than
in the failures divergences model and yet we will not lose any failures information by doing so (recall
that the conditions of the implementation relation itself are defined in terms of the failures divergences
model). This is the fact that allows us to work only in the stable failures model and thus to transform
the checking of condition LC into a check for deadlock-freedom.
bi :
Lemma 20 The following hold of Q
b i = αBi .
1. αQ
b
b t = w Bi ∧ R ⊆ αBi ∩ X}.
2. φQi = {(t, R) | (∃(w, X) ∈ φ⊥ Q)
b i = {t | w ∈ τ Q
b ∧ t = w Bi }.
3. τ Q
b and the proof of this part follows immediately.
Proof. (1) We observe that αPROCi = αQ
b = ∅ and so φQ
b = φ⊥ Q.
b
(2) By theorem 7 and the fact that conditions DP and DF have been met, δ Q
b
b
We observe that φPROCi = {(t, R) | R ⊆ αQ \ αBi }. From this we have that φ(Q k PROCi ) = {(t, R) |
b R ⊆ (αQ
b \ αBi ) ∪ (αBi ∩ X)}. The proof of this part follows from the above.
(∃(t, X) ∈ φ⊥ Q)
b ∗ and from this we have that τ (Q
b k PROCi ) = τ Q.
b The
(3) We first observe that τ PROCi = (αQ)
proof of this part follows from the above.
t
u
b i to give a process which
Before going on to define the tester process which will be composed with Q
b does not meet condition LC with respect to channel bi , we first give some
will deadlock if and only if Q
preliminary definitions and results.
8.1
Preliminary definitions and results
The following results and definitions will be used in giving the semantic characterisation of the process
b i and to show that it does indeed encode exactly the properties we wish. These
to be composed with Q
definitions will also be used when we come to consider condition RE. In what follows, the set of maximal