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 specification, amenable to automatic verification, 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 specification and model checking. This shows the usefulness of formal specification and automatic verification during the design phase of an international standard.
Modelling and verification of PREMO synchronisable 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 specification, amenable to automatic verification, 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 specification and model checking. This shows the usefulness of formal specification and automatic verification during the design phase of an international standard.File | Dimensione | Formato | |
---|---|---|---|
prod_190034-doc_55694.pdf
solo utenti autorizzati
Descrizione: Modelling and Verification of PREMO Synchronisable Objects
Tipologia:
Versione Editoriale (PDF)
Dimensione
157.34 kB
Formato
Adobe PDF
|
157.34 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.