SynchRuler: a rule-based flexible synchronization model with model checking

Flexible synchronization models cannot provide a proper way of managing user interactions that change the course of a presentation. In this paper, we present a flexible synchronization model, termed SynchRuler, which allows such user interactions including backward and skip. The synchronization rule...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on knowledge and data engineering 2005-12, Vol.17 (12), p.1706-1720
Main Authors: Aygun, R.S., Zhang, A.
Format: Article
Language:English
Subjects:
Algorithmics. Computability. Computer arithmetics
Applied sciences
Automatic control
Automatic logic units
Automation
Checkers
Collaboration
Computer science
control theory
systems
Controllers
Engineering management
Exact sciences and technology
Humans
Index Terms- Multimedia synchronization
Information systems. Data bases
Memory organisation. Data processing
model checking
Multimedia
multimedia presentations
Software
Specifications
Streaming media
Synchronism
Synchronization
synchronization rules
Teleconferencing
Temporal logic
Theoretical computing
Timing
Video sharing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Flexible synchronization models cannot provide a proper way of managing user interactions that change the course of a presentation. In this paper, we present a flexible synchronization model, termed SynchRuler, which allows such user interactions including backward and skip. The synchronization rules, which are based on event-condition-action (ECA) rules, are maintained to handle relationships among streams in SynchRuler. The synchronization rules are manipulated by the receiver-controller-actor (RCA) scheme, where receivers, controllers, and actors are objects to receive events, to check conditions, and to execute actions, respectively. The verification of a multimedia presentation specification is performed with the synchronization model. The correctness of the model and the presentation is controlled with a technique called model checking. Model checker PROMELA/SPIN tool is used for automatic verification of the correctness of LTL (linear temporal logic) formulas.
ISSN:1041-4347
1558-2191
DOI:10.1109/TKDE.2005.205