Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Using LOTOS for the Evaluation of Design Options in the PREMO Standard

    2nd BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 14th - 15th July 1997


    G.P. Faconti & M. Massink


    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 different 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.


    PDF filePDF Version of this paper (224kb)