A Formal Approach for the Presentation of Interactive Multimedia Documents

摘要

This paper present the on-going work using a formal approach for the design of Interactive Multimedia Documents 9IMDs) 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 improtant 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 p[resentation. Further on, some scheduling policies are also presented based on this model. Finally, we introduce some characteritics of the player acturally available for the presentation of IMDs based on this new model.