Information Technology Reference
In-Depth Information
Fig. 3.
Reo model of an auction process and its
mCRL2
specification
the option
with colors
can be used to add support for context-dependency as de-
scribed in Section 6. Moreover, data types of components or services coordinated
by Reo, as well as data constraints for data dependent channels such as the
Filter
or
Trans form
channel can be defined using the same interface. Note that they are
saved as annotations in the Reo model and are automatically merged in when
generating the final
mCRL2
specification. This way we can ensure that the
mCRL2
code can be regenerated at any point without manual changes if desired.
The tool further includes an integration with
mCRL2
's model checking and
state space visualization tools. In particular, we use the
mcrl22lps
tool for gen-
erating linear process specifications from
mCRL2
code,
lps2lts
and
ltsconvert
for generating and minimizing labeled transitions systems,
lps2pbes
for model
checking formulas specified in modal
μ
-calculus, and finally
ltsgraph
for visual-
izing state spaces. Related verification tools, such as CADP
4
can be integrated
in a similar fashion since they share the same format for LTSs. The integration
with CADP is not implemented as yet.
In our encoding of Reo in
mCRL2
we translate every primitive (channel, node or
component) to a separate process, which are then run in parallel. Every primitive
end corresponds to an action in this setting. Therefore, the derived specifications
usually consist of a rather large number of processes and an even larger number
of actions. However, the interaction between all these processes is rather local,
e.g. a channel communicates only with its source and target nodes.
Our experiments show that the direct approach of naively running all processes
in parallel and then performing the communication, synchronization and option-
ally the hiding operator leads to a state space explosion during the linearization.
To overcome this problem, we add processes one by one and immediately apply the
aforementioned
mCRL2
operators. We use the topology information of the
4
http://www.inrialpes.fr/vasy/cadp
