Clément Poncelet
email: clement.poncelet@ircam.fr

Florent Jacquemard
email: florent.jacquemard@inria.fr

Test methods for Score-Based Interactive Music Systems

INRIA Mutant Project Team -(UMR-9912) IRCAM -1 Place Igor-Stravinsky 75004 Paris Time Line How be sure of a Score-Based Interactive Music System's behavior during shows ? Ensuring a "guarantee" on the behavior of a complex real-time system is not trivial and requires formal method. Today, Antescofo's behavior is "manually" checked by the compositor during rehearsals. Since rehearsal performances represent just a few set of all possible interpretations of a score, this method is not rigorous.

Manual piece preparation

k k! s 0 s 1 s 2 s 3 s m s n ǧ? d α 1 ! d α n !
with "loose" synchronization strategy

s 0 s 1 s 2 s m s n s n ḡ? α 1 ! α n ! t e i +1
t e i +1 ?

Models of groups

s 0 s 1 s 2 s 3 s m s n s o s o ǧ? g? d α 1 ! d α n ! t e i +1 ?
t e i +1 ? t e i + 1 ? Models of groups with "tight" synchronization strategy

s 0 s 1 s 1 s 2 s 2 u 2 u 2 s 3 s m s n u m u m s n s o s o ǧ? ḡ? d t e i + 1 ? t e i + 1 ? α 1 ! α 1 ! α 1 ! α 1 ! d t e i + 1 ? tei + 1 ? α n ! α n ! α n ! α n ! t e i +1 ? t e i + 1
?

t e i + 1
?

t e i +1 ? s 0 s 1 s 1 s 2 s 3 s m s n s 2 s n s j s j t e i ? t e i ? d α 1 ! d α n ! α 1 ! α n-1 ! t e i +1 ! t e i +1 ! α n !
Model of group trigger The Intermediate Representation is a step toward a formal specification of Antescofo's expected behavior. It is a model of How Antescofo's reactive engine should compute its timed output for every inputs (i.e musician performances). IR can be represented with Extended Timed Input/Output Labelled Systems. Each system starting at its s 0 or s0 state and waits on an edge δ? for a fire of δ! of the symbol δ. IR is able to specify multi-clocks, concurrences, dynamic variables...

Killable

  s

  e g e n e r a t e d i n p u t t r a c e s Translating into standard formal models (i.e Timed Automaton used by the Uppaal verification suite for realtime systems) Existing tools for timesting real time systems, with an automatic test cases generation, are based on the model of network timed automaton (TA). IR arez translated into TA straightforwardly, at the prive of expressiveness loss. A set of artificial musician performances is automatically generated, with a cover guaranty (i.e quality of tests). The conformance of real traces to the formal model allows us to increase the guarantee on the stability of Antescofo at execution time.