Modeling and verification of interactive flexible multimedia presentations using PROMELA/SPIN

The modeling and verification of flexible and interactive Multimedia presentations are important for consistent presentations over networks. There has been querying tools proposed whether the specification of a multimedia presentation satisfy inter-stream relationships. Since these tools are based on the interval-based relationships, they cannot guarantee the verification in real-life presentations. Moreover, the irregular user interactions which change the course of the presentation like backward and skip are not considered in the specification. Using PROMELA/SPIN, it is possible to verify the temporal relationships between streams using our model allowing irregular user interactions. Since the model considers the delay of data, the author is assured that the requirements are really satisfied.