Timed Verification and Testing of an Interactive Music System

Florent Jacquemard
Friday, 16 May, 2014 - 14:00
Forum D
Interactive Music Systems are involved in live performances with human musicians. They react in real time to audio signals and asynchronous incoming events according to a pre-specified timed scenario called a mixed score, written in a domain specific language (DSL). They are expected to act in a reliable way,  be robust to environmental changes, unforeseen errors in input and have a predictable behavior, in particular regarding timings.
Following these strong requirements, as much efforts as possible must be taken to assess before a performance that their behavior will conform to expectations, for a given mixed score, at a level of exhaustiveness that cannot be reached during rehearsals with musicians.
In this talk we will see the application of some formal methods to evaluation of an IMS called Antescofo, developed at Ircam and used regularly in concerts worldwide.
We will introduce Antescofo’s DSL and an medium-level intermediate representation (IR) of mixed scores. Then we will present various verification and testing tasks based on timed automata models derived from the IR:
* model based conformance testing,
* the evaluation of the robustness of mixed scores to the timing variations in human performances, 
* schedulability analysis.