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

network, possibly together with data constraints for the written or read data
values. Besides describing the interface behavior of the components, constraint
automata also serve as a formal semantics for Reo [7]. In this section, we do not
go into the details of how to compose Reo channels. Instead, we use constraint
automata as a model for the network behavior directly.
Components use ports to communicate with each other via the network. Fig. 3
shows a system of components (as rectangles), their ports (as small triangles),
and the network (as a cloud). Ports can be either input or output ports (implied
by the direction of the triangles). By exogenous coordination, we mean that a
component has no direct control on how its ports are connected. A component
can only indirectly influence its connections by raising events. Events include re-
quests/announcements of services, time-outs, or acknowledgments. These events
can trigger reconfigurations of the context-aware network. A network manager
handles the events and reconfigures the network connections according to the
events. At this moment we consider the network manager to be a part of the
network and we model the peer nodes independent of a concrete implementation
of the network manager.
In this section, we model the peer nodes of the P2P system as components.
Each peer node has two sides, a client side and a server side. Each side has
a pair of request and answer ports. As a client, a peer node writes a request
(a 'key' identifying the requested data) to its cReq -port and expects the re-
sult on its cAns -port. As a server, a peer node reads a request from its sReq -
port and writes the result to its sAns -port. For two peer nodes to communicate,
the network manager has to connect the corresponding ports of the client and
the server, i.e., the cReq -port of the client with the sReq -port of the server and
the cAns -port of the client with sAns -port of the server.

2.1 Structural Interface Description

To describe the facade of a component, we declare its ports and the events the
component may raise. Below, we define two facades, ClientSide and ServerSide .The
facade Peer inherits the ports and events declared in these two and adds another
event that is needed when the two sides are combined.

facade ClientSide begin

1

port cReq : outport 2

port cAns : inport 3

sync event openCS < req : outport , ans : inport > ( in k:Data; out f : Bool ) 4

sync event closeCS < req : outport , ans : inport > () 5

end 6

facade ServerSide begin

1

port sReq : inport

2

port sAns : outport 3

sync event openSS < req : inport , ans : outport > () 4

sync event closeSS < req : inport , ans : outport > ()

5

register <> ( in keyList : List [Data ]) // async event 6

end

7