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

custom type definitions can be found in the language reference section of the
mCRL2 web site.
The mCRL2 toolset provides tools that allow users to verify software models
specifiedinthe mCRL2 language. The toolset includes a tool for converting mCRL2
specifications into a compact symbolic representation of the corresponding LTS
to speed up subsequent manipulations, yielding so-called linear process specifica-
tions (LPS), a tool for generating explicit LTSs from LPSs, tools for optimizing
and visualizing these LTSs, and many other useful facilities. A detailed overview
is provided at the mCRL2 web site.
For model checking, system properties are specified as formulae in a variant
of the modal μ -calculus extended with regular expressions, data and time. In
combination with an LPS such a formula is transformed into a parametrized
boolean equation system (PBES) and can be solved with the appropriate tools
from the toolset. Analysis at the level of LTSs is also possible by means of equiv-
alence checking (e.g., strong and branching bisimulation or trace equivalence).
In particular, the presence or absence of deadlocks/livelocks or of certain actions
can be checked straightforwardly.

4 Translating Reo to

mCRL2

In this section, we recall the rules for mapping Reo primitives (channels and
nodes) to mCRL2 processes and briefly explain how to derive composite specifi-
cations for arbitrarily complex Reo connectors (cf. [6]).
Our mapping of the basic channels reflects the constraint automata semantics
of Reo. The mCRL2 process corresponding to a channel, is based on two atomic
actions modeling data flow on its respective ends. Analogously, we introduce a
process for every node and actions for all channel ends meeting at the node.
One important aspect of our encoding is that data constraints are translated
faithfully. For this the actions corresponding to channel and node ends are ex-
tended with data parameters. In the context of a given connector, we assume
a global datatype, which we model as the custom sort Data in mCRL2 .Infact,
most channels in Reo are agnostic to the actual type of data items they carry.
Given such a global type, we can use the summation operator in mCRL2 to define
data dependencies imposed by channels. The encodings for the primitives used
in this paper are depicted in Table 2. Note that for the FIFO we need to define
an additional datatype

sort DataFIFO = struct empty ? isEmpty | full ( e : Data )? isFull ;

The encoding of the FIFO channel includes a parameter of this datatype which
allows us to specify whether the buffer of the channel is empty or full, and if it
is full, what value is stored in it.
As in the constraint automata approach, we construct nodes compositionally
out of the Merger and the Replicator primitives. A process for a node that be-
haves like an exclusive router can be defined analogously. However, in practical
situations a third type of node comes in handy, which we refer to as Join here.