Information Technology Reference
In-Depth Information
establishMediaChannel
openWithRealCodecs
openAckWithoutCodecs
selectAndEstablishbyAcceptor
establishMediaChannel
openWithoutCodecs
openAckWithRealCodecs
selectAndEstablishbyInitiator
Fig. 8.
Breaking the Atomicity of Establish a Media Channel
a select signal carrying a real codec, selected from the priority list of codecs of
the received descriptor, the media channel can be established.
Similar to the abstract model, this sequencing the Event-B model is done by
some control variables. In the first case, by execution of
openWithRealCodecs
,
a channel is added to a specific set variable,
openWithCodecsSet
and the next
event
openAckWithoutCodecs
can be executed only for a channel which is in
openWithCodecsSet
. The other events are encoded in a similar way.
5.3 Refinement 2: Breaking the Atomicity of Modify Media
Channel
Up to this level,
modify
was considered as an atomic event that simply changes
the codec of an established media channel. In this refinement we break the atom-
icity of the
modify
event. There are different ways of modifying the properties of
an established channel. The
modify
event is decomposed to sub-events in three
diagrams, presented in Fig. 9. This decomposition fulfills the modification re-
quirements which was shown in second phase of Fig. 6.
First, in Case A, after establishing a media channel the endpoint which plays
the role of the media sender can select a new codec from the list of acceptable
codecs of the receiver, which has been received at the time of establishing the
media channel.
In Case B, the receiver side of an established media channel, can send a new
list of codecs in a
describe
signal. As described in Sect. 4, the other endpoint,
has to respond to a descriptor by choosing a codec from the new list and send
it via a selector.
It is shown that each endpoint, either initiator or acceptor, can describe itself
with a new port by sending a describe signal carrying the new port property. It
is represented as Case C.
