A formal approach for the presentation of interactive multimedia documents

This paper presents the on-going work using a formal approach for the design of Interactive Multimedia Documents (IMDs) based on the RT-LOTOS formal description technique. The present work extends this approach proposing the scheduling of IMDs based on a simple and operational model obtained as a result from the reachability analysis. One important breakthrough of this model is that it is a scheduling graph that provides the control of the occurrence of non-deterministic events, such as user interactions, within valid temporal intervals so that the global synchronization constraints of the document can be fulfilled during its presentation. Further on, some scheduling policies are also presented based on this model. Finally, we introduce some characteristics of the player actually available for the presentation of IMDs based on this new model.