Information Technology Reference
In-Depth Information
The tool most closely related to the plug-in presented in this paper is Vere-
ofy [5], a model checking tool developed at the University of Dresden for the
analysis of Reo connectors. Vereofy uses two input languages, the Reo Scripting
Language (RSL), and a guarded command language called Constraint Automata
Reactive Module Language (CARML) which are textual versions of Reo and
constraint automata, respectively. Scripts in these languages are automatically
generated from graphical Reo models and are used for the verification of circuit
properties expressed in LTL and CTL-like logics. The main advantage of the tool
comparing to our work is that it can generate clear counterexamples and show
them as paths on the initial Reo circuit, while the counterexamples in
mCRL2
may be huge and not very useful. However, in contrast to our approach, Vereofy
does not support context-dependent and transformer channels, provides a for-
mat for specifying filter conditions that is less expressive than ours, and does not
allow join nodes in the circuits. Moreover, it expects the user to define a global
data domain eligible to all connectors and components in the model instead of
generating it automatically, and cannot handle recursive type definitions which
we need to deal with join nodes, for example.
Khosravi et al. [13] establishes a mapping of Reo to Alloy, a lightweight mod-
eling language based on first-order relational logic. To check the correctness of
a circuit, the desired properties are expressed in terms of assertions which are
closely related to LTL and checked by the Alloy Analyzer. The approach deals
with context dependency in Reo by defining special relations that enforce max-
imal progress in circuit execution. However, the actual values of data passed
through the channels are not considered in this work. Moreover, the authors ad-
mit to have considerable problems with performance. Bonsangue and Izadi [14]
defined semantics of context-dependent Reo connectors in terms of Buchi au-
tomata and generalized standard automata based model checking algorithms to
enable verification of LTL formulas for Reo connectors. However, this work is
purely theoretical and is not supported by any existing software tool.
Kemper [15] presented a SAT-based approach for bounded model checking of
timed constraint automata (TCA), see [16]. In this work, the behavior of TCA
is represented as formula in propositional logic with linear arithmetic which can
be analyzed by various SAT solvers. Since TCA provide operational semantics
for timed Reo, this approach can be used for model checking timed properties
of Reo connectors. However, at the moment there is no tool for generating TCA
from graphical Reo circuits. The development of such a plug-in for data-aware
Reo will require tools for analyzing data constraints and functions used in filter
and transformer channels. In our work, we map each channel to a process in the
process algebra
mCRL2
separately, and exploit the functionality provided by the
mCRL2
toolset to obtain a semantic model of the whole circuit in terms of LTS
where transitions are labeled with names parametrized with data observed in
these ports. Moreover, our approach can handle data manipulation using trans-
former channels with associated non-linear functions. Since the
mCRL2
toolset
supports time analysis, the extension of our conversion tool with the ability to
deal with timer channels is straightforward and belongs to our future work.
