6 Semantics

Thus far we have relied on the reader's good faith that the notation outlined above actually makes sense, and that the analytic techniques are sound. In this section we sketch the formal basis for this.

The basic idea is to translate the notation into pure CSP [Hoa85]. In attempting to provide such a semantics, the key difficulties are to account for the dynamic creation and deletion of processes, and to arrange things so that the alphabets of the evolving topology leads to the intended interactions. The problem, of course, is that CSP can only describe a static configuration of processes. (That is, one can't create new processes and communication channels ``on the fly"). How then can one give meaning to such actions as ``new", ``delete", etc.?

Our approach is based on two key ideas. First we restrict systems to those for which there are a finite (albeit potentially large) set of possible configurations. Second in the translation we ``tag" events with the configuration in which that event occurs. The effect of a reconfiguration action, is to cause the tags to change so that the interactions occur as defined by the new configuration. Thus an event, e, in one configuration might end up synchronizing with one process in one configuration, but with another in a different configuration.

More formally, each event p.e of the component Cp is relabelled as Cp.p.e.Cn.r when the port p of Cp is attached to the role r of the connector Cn. For example, when the Link connector interacts with the Primary server, the reply case of L is defined as:

$L.s.reply.Primary.p \rightarrow \overline{L.c.reply.C.p} \rightarrow {\bf Glue}$

Our transformation also introduces the ``plumbing" that allows selection of the proper version: each version of a transformed component begins with a $Cp.go.p_{1}.Cn_{1}.r_{1}\ldots r_{n}.Cn_{n}.r_{n}$ event selecting the version of Cp, where its port p₁ is attached to the role r₁ of Cn₁,...and its port p_n attached to the role r_n of Cn_n. For example, the connector L is compiled to:

$L = (L.go.c.C.p.s.Primary.p \rightarrow Glue_{1}) \;\Box\; (L.go.c.C.p.s.Secondary.p \rightarrow Glue_{2})$
$Glue_{1} = L.c.request.C.p \rightarrow (\overline{ L.s.request.Primary.p \rightarrow} Glue_{1} \;\Box\; \ldots$
$Glue_{2} = L.c.request.C.p \rightarrow (\overline{L.s.request.Secondary.p} \rightarrow Glue_{2} \;\Box\; \ldots$

Finally, the configuror definition is transformed into a CSP process too, where the ``new", ``del", ``attach" and ``detach" actions are compiled into the previous $Cp.go\ldots$ events that select the proper configuration of the components at each reconfiguration step. For example, the following configuror portion: $new.L \rightarrow Attach.C.p.to.L.c \rightarrow Attach.Primary.p.to.L.s \rightarrow \ldots$ is transformed to $L.go.c.C.p.s.Primary.p \rightarrow \ldots$

The formal semantics based on CSP allows us to adapt or extend the consistency and completeness analysis provided by Wright.

Most of the Wright checks can be directly adapted to the dynamic context. For example, the deadlock checks for connectors remain the same, but the terminating success events $\sqrt{}$ must be replaced by a control event triggering a connector deletion.

The port-role consistency test of Wright must be redefined in our dynamic context. Indeed, because of reconfiguration, it isn't a port which is attached to a role in a dynamic system, but a sequence of ports. For example, our previous FaultTolerantLink connector is alternatively attached to a FlakyServer and a SlowServer. A ``virtual" port defined by the sequence of ports attached to a connector role can easily be constructed with the help of the configuror.

Dynamic systems provide new opportunities for checking. For example, consistent configurors should guarantee that when the event new.C occurs, C must not already belong to the current configuration. As the configuror is defined in CSP, the test of this property can be formally expressed as CSP refinement checks:

$(prop = new.C \rightarrow (del.C \rightarrow prop \;\Box\; \S)) \sqsubseteq configuror$

Similar properties dealing with attachments can be expressed and checked in the same way.

The previous analysis ensures that the complete system is consistent. Another application of our semantics is to prove that a dynamic system (or sub-system) is equivalent to a steady-state one. For example, we could show that the two alternating servers can be merged in a bigger component with only one port, or that an extra port could be added to the client component to make the attachments static as in section 3.

Finally, we can examine the code reusability. For example, our definitions of the client component are the same in the first Client-Server steady-state system (Section 2.) and in the FaultTolerant Client-Server dynamic system (Section 4.). We did not have to introduce control events in the client definition. So, in a real implementation the same client code could be used in both steady-state and dynamic systems.