Information Technology Reference
In-Depth Information
Media Channel System
*
establishMediaChannel
modify
close
Fig. 7.
Initial Model of Media Channel System
As described before, this ordering is ensured by event guards in the Event-B
model. The abstract model contains a variable called
mediaChannel
contain-
ing established media channels, and a function
codec
which maps each estab-
lished channel to its chosen the codec. The first event,
establishMediaChannel
,
is guarded by
ch
mediaChannel
So if a channel has not been added to
mediaChannel
set, it means it has not been
established then by execution of this event it would be added to
mediaChannel
:
mediaChannel = mediaChannel
∈
}
Events,
modify
and
close
can be executed for a channel if it was established, it
is done by this guard:
ch
∪{
ch
mediaChannel
In
modify
event the codec of a channel can be changed and in
close
event, the
channel is removed from
mediaChannel
.
∈
5.2 Refinement 1: Breaking the Atomicity of Establish Media
Channel
In the abstract model, we saw that a media channel is established in a single
atomic step. However first phase of Fig. 6 has shown that establishing a media
channel is not atomic. Instead, an open request should be sent by the initiator
endpoint and should be responded to by an
openAck
signal from the acceptor
side.
Following the protocol steps of Fig. 6, breaking the atomicity of establishing a
media channel is outlined diagrammatically in Fig. 8. Two cases are possible. The
initiator can send an open signal containing a list of codecs in a descriptor and
define itself as a receiver, in this case the acceptor sends an open acknowledge
signal without any codec and then selects a codec from received list in select
signal. In this case the direction is from acceptor to initiator.
In the other case open signal does not contain a list of codecs and instead
the acceptor sends a list of codecs in open acknowledge signal and defines itself
as the receiver and the initiator selects a specific codec in select signal. The
direction in this case is from initiator to acceptor. In both cases after receiving
