Nicolas Rivière
LAAS-CNRS,
F-31077 Toulouse Cedex 4, France
nriviere@laas.fr
B. Pradin-Chézalviel
LAAS-CNRS,
F-31077 Toulouse Cedex 4, France
IUT A, UPS
chezalvi@laas.fr
R. Valette
LAAS-CNRS
F-31077 Toulouse
Cedex 4, France
robert@laas.fr
Présenté aux :
JDIR, Toulouse, 4-6 mars 2002
La conception de documents multimedia (interactifs) est aujourd'hui un domaine d'applications qui, avec la complexité des documents produits (animations graphiques, audio, video, audio-video mais avant tout temps réel) grandissante, nécessite un ordonnancement des différents éléments qui composent les documents toujours plus optimal. La prise en compte implicite de l'aspect temps réel dans ce type d'applications oblige les concepteurs à tenir compte de manière primordiale de la présentation. En effet, les documents sont conçus en fonction de la présentation que l'on veut qu'ils aient. Il apparaît donc essentiel d'avoir un ordonnancement optimal des différents éléments du document afin de pouvoir respecter toutes les contraintes temporelles liées à la présentation de ce dernier.
Afin de pouvoir ordonnancer correctement une présentation, il est nécessaire de connaître les différents ordres partiels qui permettent d'aboutir à une synchronisation correcte de tous les éléments qui composent le document multimedia.
Pour cela une technique d'ordonnancement basée sur une approche formelle pour la présentation de documents multimedia interactifs a été développée au LAAS-CNRS. La méthodologie de conception formelle de ces documents consiste à générer un graphe d'ordonnancement après plusieurs étapes. La première étape est une description du comportement du document lors de sa présentation à l'aide d'un modèle auteur de haut niveau tel que SMIL et autres. La structure temporelle et logique qui a été définie est traduite en une spécification formelle RT-LOTOS. À partir de là est dérivé un graphe d'accessibilité minimale dont on vérifie les propiétés de cohérence. Lorsque les contraintes temporelles du document sont respectées alors il est possible de générer l'ordonnancement de sa présentation ; le graphe obtenu contient tous les comportements vérifiant la cohérence du document. Dans le cas contraire, il faudra revoir la description jusqu'à satisfaire les contraintes. Cette méthodologie nous propose de générer dans un premier temps un graphe qui contient des ordres partiels vérifiant une accessibilité logique mais pas toujours temporelle. Ce qui nécessite l'élimination des branches dites inconsistantes afin d'obtenir un graphe consistant.
Nous nous proposons par notre méthode de générer directement tous les ordres partiels dits consistants qui vérifient les contraintes logiques et temporelles du document multimedia. Pour cela, nous utilisons plusieurs outils : les réseaux de Petri temporels, la logique linéaire et les TCSP (Temporal Constraint Satisfaction Problem).
Un réseau de Petri définit les relations de précédence entre les transitions. Dans la théorie de ces réseaux, l'analyse de l'accessibilité (d'un état vers un autre) est basée sur des séquences de tir dans lesquelles le franchissement des transitions apparaît dans un ordre total. L'utilisation de la logique linéaire nous permet de dériver des ordres partiels tout en conservant les relations de précédence induites par le réseau. Pour cela nous utilisons l'équivalence entre accessibilité dans un réseau de Petri et prouvabilité de séquent en logique linéaire. Ainsi, durant la preuve, toutes les contraintes générées par le réseau et le marquage initial sont vérifiées.
L'état courant d'un système informatique est le marquage courant associé au réseau modélisant le système. Ordonnancer un ensemble d'opérations est équivalent à trouver le meilleur ordre partiel parmi les tirs de transition correspondant aux opérations à faire et leur date de tir optimale. Dans notre contexte, le modèle réseau de Petri doit être complémenté par des contraintes temporelles (durées d'opérations, dates voulues, etc...). Dans notre approche, nous utilisons le modèle p-temporel car il a été montré que lors d'une traduction d'un réseau de Petri temporel en un TCSP, il était plus naturel d'associer des durées aux places plutôt qúaux transitions. Les contraintes de précédence sont en effet générées par des places.