ContactPerson: aygun@cse.buffalo.edu Remote host: wagner.cse.buffalo.edu ### Begin Citation ### Do not delete this line ### %R 2002-15 %U /home/csegrad/aygun/public_html/papers/report_model.pdf %A "Aygun, Ramazan Savas %A Zhang, Aidong" %T Rule-based Flexible Synchronization Modeling with Model Checking %D December 05, 2002 %I Department of Computer Science and Engineering, SUNY Buffalo %K Multimedia Synchronization, Model Checking, Synchronization Rules, Multimedia Presentations, Linear Temporal Logic. %X Specification as in SMIL usually considers forward presentation without considering interactions that change the course of the presentation like backward and skip. Also, management of the presentation constraints become harder when the course of the presentation changes. In this report, we introduce a synchronization model, termed RuleSync, for management of robust, consistent, and flexible presentations that include a comprehensive set of interactions. RuleSync manipulates synchronization rules that are managed by Receiver-Controller-Actor (RCA) scheme where receivers, controllers and actors are objects to receive events, to check conditions and to execute actions, respectively. The correctness of the model and the presentation is controlled with a technique called {\it model checking}. Model checker PROMELA/SPIN tool is used for automatic verification of the correctness of LTL (Linear Temporal Logic) formulas.