Istituto di Scienza e Tecnologie dell'Informazione     
Faconti G., Massink M. Modelling and verification of PREMO synchronizable objects. In: Formal Aspects of Computing, vol. 10 pp. 405 - 434. BCS, 1999.
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.
Subject Formal modelling
Model checking
Multimedia presentation
D.2.4 Software/Program Verification. Formal methods

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional