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.
Modelling and verification of PREMO synchronizable objects
Faconti G;Massink M
1998
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
prod_408286-doc_143233.pdf
solo utenti autorizzati
Descrizione: Modelling and verification of PREMO synchronizable objects
Tipologia:
Versione Editoriale (PDF)
Dimensione
163.16 kB
Formato
Adobe PDF
|
163.16 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.