Information Technology Reference
In-Depth Information
The LossyFIFO connector is a classical example where context-dependency is
required (cf. [3]). Fig. 2 depicts the corresponding labeled transition systems for
the basic constraint automata encoding (a), as well as the encoding based on the
coloring semantics (b). For simplicity, we use the singleton set Data =
{
x
}
as
data domain. The crucial point here is that in the initial state 0, the constraint
automata version can lose data (loop A ( x )), which is an unintended behavior.
However, in the coloring encoding, there is no such behavior.
A ( noflowG ) | B ( noflowR )
A ( noflowG ) | B ( noflowG )
A ( flow ( x )) | B ( noflowG )
A (
)
A ( noflowG ) | B ( noflowG )
A (
flow
( x ))
|
B (
noflowG
A ( x )
A ( x )
flow
( x ))
|
B (
noflowR
)
A ( x )
0
1
0
1
B ( x )
A ( x ) | B ( x )
(a) CA encoding
( x ))
A ( flow ( x )) | B ( flow ( x ))
(b) Coloring encoding
A (
noflowG
)
|
B (
flow
Fig. 2. Labeled transition systems for the LossyFIFO connector
Using the coloring model we can properly represent context-dependency in
mCRL2 . In contrast to [3], our encoding also reflects the state of the connectors
and can further include data-dependency at the same time. Note also that even
though the coloring encoding includes extra transitions for no-flow actions, the
number of states is equal to the constraint automata version.
7
Implementation
We implemented the conversion from Reo to mCRL2 discussed above as an exten-
sion to the Eclipse Coordination Tools (ECT), see [4]. ECT is a framework for
modeling, verification and execution of component-based and service-oriented
systems. It consists of a set of integrated tools for the Eclipse platform 3 .The
framework provides functionality for converting high-level modeling languages,
such as UML, BPMN and BPEL to Reo, for editing and animation of Reo mod-
els, generation of automata-based semantical models from Reo, modeling and
verification of QoS properties and tight integrations with external model check-
ing tools such as Vereofy [5] or PRISM [12].
From our conversion tool, an mCRL2 specification can be obtained automat-
ically from any Reo circuit simply by selecting it in the graphical Reo editor.
A screenshot of the tool is shown in Figure 3. The code generation can be cus-
tomized using various options. For instance, enabling the option with components
will allow to incorporate process definitions for the components attached at the
boundary of a connector. The option with data enables the data-aware encod-
ing. If not enabled, data parameters and constraints are omitted. Furthermore,
3 http://www.eclipse.org
 
Search WWH ::




Custom Search