Information Technology Reference
In-Depth Information
The rest of this paper is organized as follows. In Section 2, we summarize
the basics of Reo. In Section 3, we review the
mCRL2
specification language and
its toolset. In Section 4, we briefly describe the translation of Reo to
mCRL2
.In
Section 5, we formally prove the correctness of this translation. In Section 6, we
discuss the coloring semantics for Reo, a more expressive semantic model that
is able to deal with context dependency, and translate context-aware Reo to
the process algebra
mCRL2
. In Section 7, we describe an updated conversion tool
implemented as part of the Eclipse Coordination Tools (ECT) and evaluate its
performance with and without optimization techniques based on the structural
information about Reo circuits. In Section 8, we discuss related work. Finally,
in Section 9, we give concluding remarks and outline future work.
2 The Reo Coordination Language
Reo is a channel-based coordination language wherein components or services
are coordinated exogenously (from outside) by so-called
connectors
[9]. These
connectors have a graph-like structure where the edges are user-defined commu-
nication channels and the nodes implement a standard routing policy.
Channels in Reo are entities that have exactly two ends (also referred to
as
ports
), which can be either
source
or
sink
ends. Source ends accept data
into, and sink ends dispense data out of their channel. Reo allows channels to
have two source or two sink ends. Although channels can be defined by users in
Reo, a set of basic channels suces to implement rather complex coordination
protocols. One of the most basic channels in Reo is the so-called
Sync
channel,
which is a directed channel that accepts a data item through its source end if it
can instantly dispense it through its sink end. The
LossySync
channel behaves
similarly except that it always accepts data items through its source end. The
data item is transferred if it can be dispensed through the sink end, and lost
otherwise. The
SyncDrain
has two source ends and accepts data through them
simultaneously. All accepted data items are lost. The
AsyncDrain
channel accepts
data items through any of its two source ends, but never from both of them
synchronously. The
FIFO
is an asynchronous channel with a buffer of size one.
The basic set of Reo channels also includes channels that have data dependent
behavior or perform data manipulation. For instance, the
Filter
channel loses
the data item at its source end if the item does not match a certain pattern,
which is defined in terms of a data constraint for a particular instance of this
channel. Similarly one can also associate a data constraint to the
SyncDrain
.The
channel blocks if the data constraint cannot be evaluated to
true
.Furthermore,
data manipulation can be implemented using the
Transform
channel. It applies
a user-defined function to the data item at its source end and yields the result
at its sink end.
Channels can be joint together using nodes. A node can be of one out of
three types: source, sink or mixed, depending on whether all coinciding channel
ends are source ends, sink ends or a combination of both. Source and sink nodes
together form the boundary of a connector, allowing interaction with its envi-
ronment. Source nodes act as synchronous replicators, sink nodes as mergers.