Formal specifications use mathematical notations to precisely describe what properties a system need to have instead of how these properties are implemented. The Z notation is a formal specification language widely used in Europe. In this paper, we use the Z notation to analyze the temporal knowledge underlying a multimedia presentation. We then present a system based on the four temporal specification statements that we propose in this paper. The system visualize the design of a multimedia presentation. The early experience of using the system shows that it is feasible to use logic inference rules to assist the design of good multimedia presentations.
1997 international conference of multimedia computing and systems, pp.135-150