Information Technology Reference
In-Depth Information
Fig. 4.
Event-B Model Part b
Fig. 5.
Event-B Model Part c
4 An Overview of Media Channel System Requirements
and Multi Media Protocol
Media Channel Properties
All properties described in this section are based on a Spin model in [12]. This
case study has a protocol for establishing, modifying and closing a media channel.
We believe that using the atomicity decomposition technique eases understand-
ing and development of the models.
Each Media Channel has one source, one sink, a codec type and a specific
direction. A Media Channel is point-to-point and dynamic, established for trans-
ferring multi-media data.
A codec is a specific data format by which data is encoded. The codec choice
in the media channel is dynamic; it means that each endpoint of the channel
is allowed to change the codec in the middle of data transfer. Although each
endpoint can interpret more than one codec, the source and sink of a media
channel have to know which codec they are supposed to send or receive with. So
any two endpoints of a media channel should have at least one common codec.
Note that in our Event-B model, we are not modeling just a single media
channel, rather we are modeling a system that manages an arbitrary number
