Verification of Context-Dependent Channel-Based Service Models - Formal Methods for Components and Objects - page 33

The hiding operator as introduced in [2] differs from the hiding operator pre-
sented here. In [2], in a context of language equivalence for timed data streams,
an arbitrary number of transitions with flow exclusively over hidden ports are
combined within a single observable transition. In our set-up, a computation
of the C -restricted automaton corresponds transition-by-transition to a com-
putation of the unrestricted automaton. Note that the minimization of the C -
restricted automaton by aggregating several transitions into a weak one can be
done afterward, as branching bisimulation remains preserved.

6 Coloring Semantics

The constraint automata semantics used in the previous section has a major
drawback: it cannot model context-dependency. For example, the LossySync
channel is not correctly represented as its constraint automaton can pass or
lose data non-deterministically, whereas according to its informal semantics the
passing of data has priority over losing. To cope with this problem, different
semantical models have been introduced. One of them is the so-called coloring
semantics. The basic idea in this model is to associate flow and no-flow colors
to channel ends. Clarke et al. showed in [3] that one flow color and two no-
flow colors are su cient to model context-dependency such as required by the
LossySync . The names and graphical representations of these colors are shown
in Figure 1(a).

Sync LossySync Merger

(1)
(2)
(3)
(4)

(1)
(2)
(3)
(4)

(1) (2)

Name Symbol

flow
no-flow-give-reason
no-flow-require-reason

(3) (4)

(b) Colorings for some Reo channels and nodes

(a) Colors

Fig. 1. Colors and examples of coloring semantics for Reo channels and nodes

Valid behaviors of channels are then expressed as colorings of their respective
ends. Figure 1(b) depicts the colorings of the Sync , LossySync and Merger prim-
itives. Note that the colors are always read from the perspective of the adjacent
nodes. For instance, in coloring (2) of the Sync the sink node gives a reason for
no flow, whereas the source node requires a reason. This models the behavior
where data is available at the source end but the receiver at the sink end is not
ready to accept data. Similarly, in coloring (3) there is no flow, because there
is no data available at the source end. Finally, coloring (4) models the situation
where no data is available and the receiver is also not ready to accept any data 2 .

2 This behavior is implied by the so-called flip-rule in [3].