Information Technology Reference
In-Depth Information
x > 5
i
nvoke[openSS][self][Peer]
!
deadline = XD
invoke[confirmSS][Peer][self]?
reg_upd[Peer]!
invoke[register][self][Peer]!
deadline = MD
x > 5
invoke[closeSS][self][Peer]!
deadline = MD, x = 0
oc_os?
x = 0
x > 5
invoke[openCS][self][Peer]!
deadline = XD
invoke[confirmCS][Peer][self]?
open_upd[Peer]?
reg_upd[Peer]?
x > 5
invoke[closeCS][self][Peer]!
deadline = MD, x = 0
invoke[update][self][Peer]!
deadline = XD
x = 0
open_upd[Peer]!
oc_os!
Fig. 13.
The behavioral interface of broker modeled in timed automata
invoke[message][sender][ receiver ]!
. To specify the deadlines associated to a message, we
use the variable
deadline
.
In Fig. 13, we use the
open upd
and
reg upd
channels to synchronize the automata
for
Peer
with
ClientSide
and
ServerSide
, respectively. Additionally, the automata for
ClientSide
and
ServerSide
are synchronized on the
oc os
channel; this abstractly mod-
els the synchronization on port communication between the components in which
the network manager is not directly involved. This model allows the client side of
any peer to connect to the server side of any peer (abstracting from the details of
matching the peers).
The
confirmCS
and
confirmSS
messages model the confirmation sent back from the
network manager to the open session requests by the peers. In the implementa-
tion, this is an implicit reply which is therefore not modeled in the behavioral
interfaces of the peers in Section 2.2. These edges synchronize with the method
implementations (explained next) in order to reduce the nondeterminism in the
model.
Methods.
The methods also use the
invoke
channel for sending messages. Fig. 14
shows the automata implementation of two methods for handling the
openCS
and
register
events. In
openCS
, and similarly in every method, the keyword
caller
refers
to the object/component that has called this method. The scheduler should be
able to start each method and be notified when the method finishes, so that it can
start the next method. To this end, method automata start with a synchroniza-
tion on the
start
channel, and finish with a transition synchronizing on the
finish
x >= 1
invoke[confirmClient][caller][self]!
x == 1
x <= 1
x <= 1
finish[self]!
finish[self]!
start[openCS][self]?
x = 0
start[register][self]?
x = 0
Fig. 14.
Method automata for handling openCS and register events
