The Credo Methodology - Formal Methods for Components and Objects - page 49

sReq cReq
N1
sAns cAns

sReq cReq
N3
sAns cAns sReq cReq

N2
sAns cAns

Fig. 5. Using Reo channels for modeling the network

The overall behavior of the system is described by the synchronized product
of the Broker , the component automata, and the channel automata. The network
itself consists of the Broker and the channels. Fig. 5 shows a configuration in
which two buffer channels are used as the network connecting the components.
The dashed arrows in this figure show port bindings, i.e., the channel-end to
which a port is bound. The bold arrows represent the channels.

3 Dataflow Model

In this section we give a detailed model of the dataflow of our peer-to-peer
example. We use the Ve r eo fy [10,6,11] (see Fig. 6) tool suite for modeling and
analyzing the detailed dataflow model. The Ve r eo fy tool suite supports model
checking and equivalence checking of components, connectors, and the composite
system. Constraint automata serve as a generic operational semantics, which is
used for the service interfaces of the components, the network that provides the
glue code, and the composite system.

Constraint Automata
Reactive Module
Language (CARML)

Reo scripting language
(RSL)

LIBRARIES
(pre- and user defined)

Symbolic CA
Representation

graphical representation
of the network

graphical representation
of the constraint automaton

Model Checker
(LTL, BTSL, ASL)

Bisimulation Checker

YES/ NO + witness/couterexample
(graphical and textual representation)

YES/ NO

Fig. 6. The Vereofy tool suite