Modeling and verification of interactive flexible multimedia presentations using PROMELA/SPIN

Ramazan Savas Aygün; Aidong Zhang

doi:10.1007/3-540-46017-9_15

Modeling and verification of interactive flexible multimedia presentations using PROMELA/SPIN

Ramazan Savas Aygün
, Aidong Zhang

Department of Computer Science and Engineering

SUNY Buffalo

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

10 Scopus citations

Abstract

The modeling and verification of flexible and interactive multimedia presentations are important for consistent presentations over networks. There has been querying tools proposed whether the specification of a multimedia presentation satisfy inter-stream relationships. Since these tools are based on the interval-based relationships, they cannot guarantee the verification in real-life presentations. Moreover, the irregular user interactions which change the course of the presentation like backward and skip are not considered in the specification. Using PROMELA/SPIN, it is possible to verify the temporal relationships between streams using our model allowing irregular user interactions. Since the model considers the delay of data, the author is assured that the requirements are really satisfied.

Original language	English
Title of host publication	Model Checking Software - 9th International SPIN Workshop, Proceedings
Editors	Dragan Bosnacki, Stefan Leue
Publisher	Springer Verlag
Pages	205-212
Number of pages	8
ISBN (Print)	3540434771, 9783540434771
DOIs	https://doi.org/10.1007/3-540-46017-9_15
State	Published - 2002
Event	9th International SPIN Workshop on Model Checking Software, SPIN 2002 - Grenoble, France Duration: Apr 11 2002 → Apr 13 2002

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2318 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th International SPIN Workshop on Model Checking Software, SPIN 2002
Country/Territory	France
City	Grenoble
Period	04/11/02 → 04/13/02

Access to Document

10.1007/3-540-46017-9_15

Cite this

Aygün, R. S., & Zhang, A. (2002). Modeling and verification of interactive flexible multimedia presentations using PROMELA/SPIN. In D. Bosnacki, & S. Leue (Eds.), Model Checking Software - 9th International SPIN Workshop, Proceedings (pp. 205-212). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2318 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-46017-9_15

Aygün, Ramazan Savas ; Zhang, Aidong. / Modeling and verification of interactive flexible multimedia presentations using PROMELA/SPIN. Model Checking Software - 9th International SPIN Workshop, Proceedings. editor / Dragan Bosnacki ; Stefan Leue. Springer Verlag, 2002. pp. 205-212 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d7795c2228844f7f8be9c309129c1c07,

title = "Modeling and verification of interactive flexible multimedia presentations using PROMELA/SPIN",

abstract = "The modeling and verification of flexible and interactive multimedia presentations are important for consistent presentations over networks. There has been querying tools proposed whether the specification of a multimedia presentation satisfy inter-stream relationships. Since these tools are based on the interval-based relationships, they cannot guarantee the verification in real-life presentations. Moreover, the irregular user interactions which change the course of the presentation like backward and skip are not considered in the specification. Using PROMELA/SPIN, it is possible to verify the temporal relationships between streams using our model allowing irregular user interactions. Since the model considers the delay of data, the author is assured that the requirements are really satisfied.",

author = "Ayg{\"u}n, \{Ramazan Savas\} and Aidong Zhang",

year = "2002",

doi = "10.1007/3-540-46017-9\_15",

language = "English",

isbn = "3540434771",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "205--212",

editor = "Dragan Bosnacki and Stefan Leue",

booktitle = "Model Checking Software - 9th International SPIN Workshop, Proceedings",

address = "Germany",

note = "9th International SPIN Workshop on Model Checking Software, SPIN 2002 ; Conference date: 11-04-2002 Through 13-04-2002",

}

Aygün, RS & Zhang, A 2002, Modeling and verification of interactive flexible multimedia presentations using PROMELA/SPIN. in D Bosnacki & S Leue (eds), Model Checking Software - 9th International SPIN Workshop, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2318 LNCS, Springer Verlag, pp. 205-212, 9th International SPIN Workshop on Model Checking Software, SPIN 2002, Grenoble, France, 04/11/02. https://doi.org/10.1007/3-540-46017-9_15

Modeling and verification of interactive flexible multimedia presentations using PROMELA/SPIN. / Aygün, Ramazan Savas; Zhang, Aidong.
Model Checking Software - 9th International SPIN Workshop, Proceedings. ed. / Dragan Bosnacki; Stefan Leue. Springer Verlag, 2002. p. 205-212 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2318 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Modeling and verification of interactive flexible multimedia presentations using PROMELA/SPIN

AU - Aygün, Ramazan Savas

AU - Zhang, Aidong

PY - 2002

Y1 - 2002

N2 - The modeling and verification of flexible and interactive multimedia presentations are important for consistent presentations over networks. There has been querying tools proposed whether the specification of a multimedia presentation satisfy inter-stream relationships. Since these tools are based on the interval-based relationships, they cannot guarantee the verification in real-life presentations. Moreover, the irregular user interactions which change the course of the presentation like backward and skip are not considered in the specification. Using PROMELA/SPIN, it is possible to verify the temporal relationships between streams using our model allowing irregular user interactions. Since the model considers the delay of data, the author is assured that the requirements are really satisfied.

AB - The modeling and verification of flexible and interactive multimedia presentations are important for consistent presentations over networks. There has been querying tools proposed whether the specification of a multimedia presentation satisfy inter-stream relationships. Since these tools are based on the interval-based relationships, they cannot guarantee the verification in real-life presentations. Moreover, the irregular user interactions which change the course of the presentation like backward and skip are not considered in the specification. Using PROMELA/SPIN, it is possible to verify the temporal relationships between streams using our model allowing irregular user interactions. Since the model considers the delay of data, the author is assured that the requirements are really satisfied.

UR - https://www.scopus.com/pages/publications/84893611425

U2 - 10.1007/3-540-46017-9_15

DO - 10.1007/3-540-46017-9_15

M3 - Conference contribution

AN - SCOPUS:84893611425

SN - 3540434771

SN - 9783540434771

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 205

EP - 212

BT - Model Checking Software - 9th International SPIN Workshop, Proceedings

A2 - Bosnacki, Dragan

A2 - Leue, Stefan

PB - Springer Verlag

T2 - 9th International SPIN Workshop on Model Checking Software, SPIN 2002

Y2 - 11 April 2002 through 13 April 2002

ER -

Aygün RS, Zhang A. Modeling and verification of interactive flexible multimedia presentations using PROMELA/SPIN. In Bosnacki D, Leue S, editors, Model Checking Software - 9th International SPIN Workshop, Proceedings. Springer Verlag. 2002. p. 205-212. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-46017-9_15

Modeling and verification of interactive flexible multimedia presentations using PROMELA/SPIN

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this