SPECIFICATION AND VERIFICATION OF MULTIMEDIA SYNCHRONIZATION SCENARIOS USING TIME-ESTELLE

Multimedia synchronization scenario modelling can be classified into f our categories: axes-based model; synchronization point control; event -based model; and interval-based model.(1) Existing formal languages d o not support the specifications and verifications of all these four c ategories of synchronization scenarios. Estelle,(2) an internationally standardised Formal Description Technique (FDT), unfortunately does n ot have enough expressive power to specify the time-dependent behaviou rs of a multimedia system. To address this limitation, we have develop ed an extended Estelle, called Time-Estelle(3) to express multimedia Q oS parameters, to identify various types of media objects, to describe temporal and spatial relationships, and to specify a range of synchro nization scenarios. This paper discusses how Time-Estelle can be used for specifying the four categories of synchronization scenarios, and d escribes how these scenarios can be verified for correctness, thus ena bling any potential temporal inconsistencies to be identified. (C) 199 8 John Wiley & Sons, Ltd.