Authoring and Automatic Verification of Interactive Multimedia Scores

Abstract

The advances in authoring of interactive scores call for a thorough analysis of the written scores. A possible way to ensure correctness of an interactive score is through the use of formal techniques such as model checking. In this work, we present a visual model of the inter-media sequencer i-score and we propose a Timed Automata encoding to reason about the interactive scores written in this software. The verification of some properties of interactive scores is presented, along an evaluation of the performance of the model-checking process with uppaal.

Keywords:

• interactive multimedia scenarios
• model checking
• performance analysis
• timed automata
• UPPAAL

Acknowledgements

We thank the anonymous reviewers for their detailed comments that helped us to improve this paper. Also, we would like to thank Jean-Michel Couturier for his valuable remarks about the paper.

Notes

Jaime Arias, LaBRI, UMR 5800, University of Bordeaux, F-33400 Talence, France.

1 https://cycling74.com

2 https://puredata.info

3 Open Sound Control (OSC) is a protocol for communication among multimedia devices (http://opensoundcontrol.org)

4 http://www.i-score.org

5 http://www.bachproject.net/

6 https://www.it.uu.se/research/group/darts/uppaal/benchmarks/

7 http://www.inria.fr/equipes/poset

8 http://scrime.labri.fr/

Additional information

Funding

This work was supported by the French agency for research (ANR) project OSSIA [grant number ANR-12-CORD-0024]; the PoSET project⁷; SCRIME⁸ (Studio de Création et de Recherche en Informatique et Musiques Expérimentales) and the ANRT CIFRE convention [grant number 1181/2014].