Using LOTOS for the evaluation of design options in the PREMO standard

PREMO, 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. The standard is written using an Object Oriented approach. In this paper we specify the behavioural aspects of one of the central objects of the standard, the PREMO synchronizable object, in a constraint oriented style. We show that by adding further constraints in a modular way various design options can be investigated by means of model checking. This provides designers with more reliable information concerning the behavioural aspects of di?erent designs which obviously is helpful in the evaluation of design decisions. In this way formal methods do not only play a role in the ?nal evaluation of the correctness of a design, but can be used in a design methodology in which a more dynamical process of design and evaluation is required. A requirement for this way of working is modularity which is well supported by both the Object Oriented and the Constraint Oriented approaches.