Le rôle d'un système d'interaction musicale (IMS) est d'accompagner les musiciens directement lors de performances (en live), comme le ferait un véritable musicien.
Il réagit en temps réel à des signaux audios, venant de musiciens, tout en suivant une spécification temporisée. Celle-ci est appelée une partition mixte et écrite dans un langage dédié (DSL). Ces action nécessitent un grand besoin de fiabilité temporelle et d’une résistance/stabilité aux erreurs d'entrée, peu étudiées dans la communauté de l'informatique musicale.

Nous présentons des techniques de tests basés sur modèle et des outils que nous appliquons à l'IMS, Antescofo.
Notre approche consiste en des scénarios de tests entièrement automatisés, depuis la spécification jusqu'à l'exécution et le verdit.
Elle fonctionne en plusieurs étapes :
(i) La compilation d'une partition mixte vers un modèle décrivant le comportement temporisé attendu de l'IMS pendant un jeu musical sur la partition.
(ii) La génération de données d'entrée pertinentes pour nos tests, comprenant des valeurs temporisées et suivant un critère de couverture.
(iii) Un calcul des sorties attendues correspondantes, selon les sémantiques des partitions mixtes.
(iv) Une exécution "boite noire" des données de test et la création du verdict.

Cette méthode a été appliquée sur une benchmark et des partitions mixtes utilisées en concert. Les résultats obtenus nous ont permis d'identifier des bugs sur l'IMS cible.

• """""" * """""" * * """""" * """""" * * """""" * """""" * * """""" * """""" * * """""" * """""" * * """""" * """""" *

Abstract:

Score-Based Interactive Music Systems (SBIMS) such as Antescofo are involved in live performances with human musicians, reacting in realtime to audio signals and asynchronous incoming events according to a pre-specified timed scenario called a mixed score.
This implies strong requirements of reliability and robustness to unforeseen errors in input.
We present the application to SBIMS’s of formal methods for black-box conformance testing of embedded systems, and describe how we have handled the 3 main problems in automatic testing reactive and realtime software like SBIMS's:
(i) the generation of relevant input data for testing, including delay values, with the sake of exhaustiveness,
(ii) the computation of the corresponding expected output, according to a given mixed score,
(iii) the test execution on input and verdict.

Our approach is based on formal models compiled from mixed scores.
Using a symbolic checker, such a model is used both for (i), by a systematic exploration of the state space of the model, and for (ii) by simulation on a given test input.
Moreover, we have implemented several scenarios for (iii), corresponding to different boundaries for the implementation under test (black box).
The results obtained from this formal test method have permitted to identify bugs in Antescofo.