Premium
Specification and verification of multimedia synchronization scenarios using time‐Estelle
Author(s) -
Tsang Tony,
Lai Richard
Publication year - 1998
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/(sici)1097-024x(199809)28:11<1185::aid-spe197>3.0.co;2-p
Subject(s) - computer science , correctness , synchronization (alternating current) , range (aeronautics) , expressive power , point (geometry) , event (particle physics) , control (management) , interval (graph theory) , distributed computing , formal description , quality of service , real time computing , theoretical computer science , programming language , computer network , artificial intelligence , channel (broadcasting) , materials science , geometry , mathematics , physics , quantum mechanics , combinatorics , composite material
Multimedia synchronization scenario modelling can be classified into four categories: axes‐based model; synchronization point control; event‐based model; and interval‐based model. 1 Existing formal languages do not support the specifications and verifications of all these four categories of synchronization scenarios. Estelle, 2 an internationally standardised Formal Description Technique (FDT), unfortunately does not have enough expressive power to specify the time‐dependent behaviours of a multimedia system. To address this limitation, we have developed an extended Estelle, called Time‐Estelle 3 to express multimedia QoS parameters, to identify various types of media objects, to describe temporal and spatial relationships, and to specify a range of synchronization scenarios. This paper discusses how Time‐Estelle can be used for specifying the four categories of synchronization scenarios, and describes how these scenarios can be verified for correctness, thus enabling any potential temporal inconsistencies to be identified. © 1998 John Wiley & Sons, Ltd.