Proving temporal consistency in a new multimedia synchronization model

Abstract

This paper introduces a new synchronization model for the formal specification of multimedia documents. By this approach, an user is able to formalize his document by hierarchically composing a set of presentation and constraint objects which are then automatically translated into a complete RT-LOTOS formal specification (RT-LOTOS is a temporal extension of the standard LOTOS Formal Description Technique) . Verification of a multimedia document aiming to identify potential temporal inconsistencies is then performed using standard reachability analysis developed and implemented for RT-LOTOS. KEYWORDS Multimedia-Hypermedia, Temporal Synchronization, Formal Specification and Verification, LOTOS, RT-LOTOS INTRODUCTION Multimedia documents represent a powerful method of communication integrating a variety of media with different temporal characteristics, e.g. time dependent media such as video, audio or animation, and time independent media, such as text, graphics and images. A central i...