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.
 
Search WWH ::




Custom Search