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

at the interface ports, and state assignments describe the effect on the local
variables. An I/O-guard specifies the list of active ports as well as restrictions
to the data observed at the active ports. E.g., the I/O-guard “

& # A == k ”
states that port A is the only port active during the transition and the observable
data value at A is equal to k .
To reduce the complexity of our model for demonstration purposes we (1)
abstract from the update events, (2) assume that all peers have all data, and
(3) the network manager establishes a connection to server i if data i is requested.
Furthermore, we use a global data domain

{ }

A

Data = { 0 , 1 , 2 , 3 ,

key 0 , key 1 , key 2 ,
data 0 , data 1 , data 2 ,
openSignal , closeSignal , registerSignal ,

} undefined

for the requests, the data and all signals. The numbers 0 , 1 , 2 , 3 Data are used as

signals triggering a reconfiguration in the network topology. Please note, that for
each message type a distinct input or output port has been introduced according
to the facades definition from Section 2.1. An alternative way of modeling uses

∈

MODULE ClientSide {

1

// interface declaration (specification of I/O - ports):

2

in : openCS ;

3

in : closeCS ;

4

out : myReq ;

5

in : myAns ; 6

// local variables: 8

var : enum{ idle , open , waiting , done } status: = idle ;

9

var : Data tans : = undefined ; 10

// transition definitions:

12

status == idle -[ { openCS }&# openCS == openSignal ]->

13

status: = open ;

14

status == open -[ { myReq }&# myReq == key0 ]-> status: = waiting ;

16

status == open -[ { myReq }&# myReq == key1 ]-> status: = waiting ;

17

status == open -[ { myReq }&# myReq == key2 ]-> status: = waiting ;

18

status == waiting -[ { myAns }]-> status: = done & tans: =# myAns ;

20

status == done -[ { closeCS }&# closeCS == closeSignal ]->

22

status: = idle & tans: = undefined ;

23

}

24

Fig. 7. CARML module for client facade of a peer