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

register openSS openCS

sReq cReq

closeSS closeCS

sAns cAns

(a) ServerSide (b) ClientSide

cAns

register

update

(c) Peer

Fig. 4. Behavioral interfaces for facades

action (read or write) is understood from the port type (given in the structural
facade description).
Fig. 4 shows the behavioral specification for the facades in our example. As
mentioned earlier, the port actions are enclosed by opening and closing session
events in Fig. 4(a) and Fig. 4(b). A server registers its data with the network
manager at initialization. We opt for a simple scenario, i.e., each server or client
handles only one request at a time. We also assume at this level of abstraction,
that openCS is always successful, i.e., every data item searched for is available.
The Peer facade inherits the behavior specified for ClientSide and ServerSide fa-
cades. The Peer facade introduces some additional behavior, i.e., an update to the
data stored at the broker. The Peer automaton (see Fig. 4(c)) synchronizes with
the ServerSide automaton (see Fig. 4(a)) to ensure that an update only takes place
after the data is registered. Moreover, the data at the broker is updated after
receiving new information (on the ClientSide ). This is modeled by synchronization
on the read operations on the cAns -port.
The behavior of the sub-type has to be a refinement of the behavior of its
super-type [28]. This is achieved by computing the product of the automata
describing the inherited behavior ( ServerSide and ClientSide ) and the automaton
synchronizing them ( Peer ). In this product [4] transitions with different action
names are interleaved while those with common action names are synchronized.

Network. The Broker in a peer-to-peer system connects the ports and handles
the events of the components. We show how to model the synchronization of a
system consisting of a fixed number of components, say n ,forsome n> 0. The
observable actions of the i -th component ( i ), i.e., the communica-

tionsonitsportsanditsevents,aredenotedby openCS i , openSS i , closeCS i ,
closeSS i , cReq i , sReq i , cAns i ,and sAns i . Synchronization of actions is modeled
in the following automata by a transition labeled with the participating actions.
For clarity, we start with different automata for the synchronization of ports
and events. Synchronization between the ports of a pair of components i and j
is described by the following automaton.

∈{ 1 ,...,n }