Sémantique formelle et vérification automatique de scénarios hiérarchiques multimédia avec des choix interactifs

Abstract

Notre propos est la conception assistée par ordinateur des scénarios comprenant des contenus multimédia qui interagissent avec les actions extérieures, notamment celles de l’interprète (e.g., spectacles vivants, installations muséales interactives et jeux vidéo). Le contenu multimédia est structuré dans un ordre spatial et temporel selon les exigences de l’auteur. Par conséquent, la complexité potentiellement élevée de ces scénarios nécessite des langages de spécification adéquats pour leur complète description et vérification.Partitions Interactives est un formalisme qui a été proposé comme un modèle pour la composition et l’exécution des scénarios multimédias interactifs. En outre, un séquenceur inter-médias, appelé ISCORE,a été élaboré à partir de la sémantique Petri net proposée par ce formalisme. Au cours des dernières années, I-SCORE a été utilisé avec succès pour la composition et l’exécution des spectacles et des expositions interactives. Néanmoins, ces applications et les applications émergentes telles queles jeux vidéo et les installations muséales interactives, de plus en plus exigent deux caractéristiques que la version stable actuelle de I-SCORE ainsi que son modèle sous-jacent ne supportent pas : (1)des structures de contrôle flexibles comme des conditionnelles et des boucles ; et (2) des mécanismes pour la vérification automatique de scénarios.Dans cette thèse, nous présentons deux modèles formels pour la composition et la vérification automatique de scénarios interactifs multimédia avec des choix interactifs, i.e., des scénarios où l’interprète ou le système peut prendre des décisions au sujet de leur état d’exécution avec un certain degré de liberté définie par le compositeur.Dans notre première approche, nous définissons un nouveau langage de programmation appelé REACTIVEIS dont les programmes sont définis comme des arbres représentant l’aspect hiérarchique des scénarios interactifs et dont les noeuds contiennent les conditions nécessaires pour démarrer et arrêter les objets temporels (TOS). En outre, nous définissons une sémantique opérationnelle basé sur des arbres marqués, contenant dans leurs noeuds, les informations sur le début et la fin de chaque TO. Nous définissons également une interprétation déclarative de REACTIVEIS comme formules de la logique linéaire intuitionniste avec sous exponentiels (SELL). Nous montrons que cette interprétation est adéquate : les dérivations dans la logique correspondent à des traces du programme et vice-versa.Dans notre deuxième approche, nous présentons un système basé sur des Automates Temporisés.Dans le système proposé, nous modélisons des scénarios interactifs comme un réseau d’automates temporisés et les étendons avec des points interactifs gardés par des conditions, permettant ainsi la spécification de comportements avec branchements. Par ailleurs, nous profitons des outils matures et efficaces pour simuler et vérifier automatiquement des scénarios modélisés comme des automates temporisés. Dans notre système, les scénarios peuvent être synthétisés dans un matériel reconfigurable afin de fournir une faible latence et l’exécution en temps réel.Dans cette thèse, nous explorons également une nouvelle façon de définir et mettre en oeuvre des scénarios interactifs, visant à un modèle plus dynamique en utilisant le langage réactif REACTIVEML.Enfin, nous présentons une extension des scénarios interactifs utilisant des réseaux de Petri colorés(CPN) qui vise à traiter des données complexes, en particulier, les données statiques et dynamiques de flux audio.