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

We use the specification languages Reo Scripting Language (RSL) for Reo
and the Constraint Automata Reactive Module Language (CARML) to spec-
ify service interfaces of the components. While the scripting language RSL is
used to specify exogenous or endogenous coordination mechanisms, the guarded
command language CARML is used to specify behavioral component interfaces
and component connectors. Both languages rely on the same semantic automata
model. This hybrid approach allows nesting of the two specification languages,
supports compositional design, modular verification and reusability of compo-
nents and component connectors. Ve r eo fy includes symbolic model checking tools
for linear-time, branching-time and alternating-time temporal logics [24,23,5]
with special operators to reason about the events and dataflow at I/O-ports of
components and internal nodes of the connecting network. Furthermore Ve r eo fy
includes a bisimulation checker [9] for components, component connectors, and
the composite system.
In the following we show how to model the network manager establishing
connections in our running peer-to-peer example. We use CARML to provide
textual specifications of the facades of server and client side and RSL to specify
the network manager. Finally we explain how the model checking engine of
Ve r eo fy is used to validate the composite system. The full source code for the
P2P model is available on the web:

http://www.vereofy.de/download/examples/vereofy_p2p_example.zip

3.1 Modeling in Vereo fy

The facades from Section 2 serve as a starting point to model the server and client
side. Facades define the interface ports together with the possible events. In this
section we follow an exogenous modeling approach where the communication
and coordination of the peers is handled completely outside the components by
the connecting network. Thus, there are no complex events inside the component
specifications, i.e., the CARML code for the server and client side. Instead, events
are handled by the network manager using synchronous message passing via I/O-
ports. The specification of I/O-ports in CARML differs only syntactically from
the facade definition presented earlier.

The Server side and client side facades in . The automata from

Section 2 for the server side and client side facades are directly translated into
CARML modules. A CARML specification consists of a (possibly empty) list of
parameter (e.g. the number of I/O-ports), the interface declaration where source
ports (for the input-ends) and sink ports (for the output-ends) of a component
and its local variables are defined followed by the transition definitions speci-
fying the behavioral interface. The evaluations of the local variables represent
automata states. The transition definitions have the form

Vereo fy

state guard − [ I/O guard ] → state assignments ;

where the state guard represents a boolean expression on the current evaluation
of the variables, I/O guard is a boolean expression on the dataflow observed