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 difierent designs which obviously is helpful in the evaluation of design decisions. In this way formal methods do not only play a role in the final 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.
Content
Author and article information
Conference
Publication date:
July
1997
Publication date
(Print):
July
1997
Pages: 1-20
Affiliations
[0001]CNR - Istituto CNUCE, Via S.Maria 36
56126 PISA, Italy