Modelling and verification of PREMO synchronizable objects

The PREMO standard, Presentation Environment for Multimedia Objects, is a major new standard under development within ISO/IEC. It addresses the creation of, presentation of, and interaction with all forms of information using single or multiple media. In this paper we give a formal LOTOS speci cation, amenable to automatic veri cation, of the PREMO synchronisable object, which is one of the central parts of the standard. Various design options are investigated by a combination of constraint oriented speci cation and model checking. This shows the usefulness of formal speci cation and automatic veri cation during the design phase of an international standard.