Compile-time error detection in temporal specifications for interactive multimedia applications

Interactive multimedia application (IMA) has been emerged as a hot-spot trend with the advance of technology to handle sound and motion video. But, it is still difficult to build IMA since it gets more complex to specify the temporal and spatial synchronizations and interactions with users inherent in IMA as the complexity of IMAs grows. In this paper, we suggest that an advanced authoring system should be facilitated with compile-time error detection to handle complex IMAs. We also propose a formal specification and verification mechanism, to detect the specification errors. In our system, the specification is carried out via top-down approach, which means that a rough specification of an IMA is completed and each component of the rough specification is specified in more detail. The detailed descriptions are verified to be equivalent to its rough descriptions, which detects the specification errors inherent in the detailed descriptions. We show the usefulness of the specification and specification mechanism via illustrating an example to specify an IMA