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

protocols. Along with the graphical notation and intuitive meaning of channel
behavior, several formal semantic models for Reo have been proposed [2,3]. This
makes it possible to analyze the connector behavior automatically using simula-
tion and model checking techniques as well as to generate executable code from
graphical models. However, these semantic models, in particular constraint au-
tomata [2] and coloring semantics [3], require the development of special software
tools to deal with them. For example, Reo animation and simulation engines [4]
are developed as Eclipse plug-ins at CWI in Amsterdam to animate and simulate
the execution of Reo circuits based on coloring semantics, and Vereofy [5] is a
model checking tool developed by the University of Dresden to check properties
of constraint automata.
Since the tailored development of reliable verification tools is a substantial
effort requiring man power over an extensive time span to mature, we chose an
alternative approach. In our recent work [6], we presented a framework for spec-
ifying behavior of Reo in mCRL2 , a specification language based on the process
algebra ACP, including time and data [7]. Specifications in this language can be
analyzed by an extensive set of model checking and simulation tools available in
the mCRL2 toolset. The mCRL2 model checker has proven its suitability for analyz-
ing large scale industrial systems. Moreover, a specification can be converted into
a labelled transition system (LTS) in various formats and subsequently be used
as input for external model checking tools, e.g., CADP [8]. The mCRL2 specifica-
tion language provides means to deal with algebraic data types and user-defined
functions. These features are essential for enabling data-aware analysis of Reo
circuits which may accept as input structured data elements from web services
and may transform them (e.g., merge, duplicate, reorder) using filter and trans-
former channels.
We developed a conversion tool that generates mCRL2 specifications from Reo
graphical models. These specifications are generated fully automatically and do
not require any manual refinement. The mapping from Reo to mCRL2 is performed
according to the constraint automata semantics of Reo. In this paper, we estab-
lish the correctness of this mapping by proving the bisimilarity of the generated
mCRL2 specification and constraint automata semantics for a given Reo circuit.
Secondly, we propose a method of step-wise mCRL2 specification generation, that
incorporates the structural information of a Reo circuit. Experimental results in-
dicate reduced execution times for linearization of the specification, a necessary
step when exploiting the mCRL2 toolkit. Finally, we incorporate coloring informa-
tion in our Reo to mCRL2 encoding. Coloring semantics have been introduced ini-
tially to provide an animated execution of Reo circuits. In contrast to constraint
automata in their basic form, coloring semantics is able to express the behavior
of context-dependent Reo channels, i.e., channels whose behavior depends on the
states of other channels or components. A basic example of such channels is a syn-
chronous lossy channel that loses data only if it cannot simultaneously dispense
it. We present an extension of our conversion tool that maps Reo channels into
mCRL2 processes that explicitly propagate the information about their states to
other parts of the circuit by means of typed actions.