DEA "INFORMATIQUE : SYSTEMES
& COMMUNICATIONS"
ANNEE 2000/2001
RESPONSABLE : Muriel Jourdan
TEL : 04.76.61.53.58
ADRESSE ELECTRONIQUE : Muriel.Jourdan@inrialpes.fr
LABORATOIRE ET EQUIPE : Projet Opéra
INRIA Rhône-Alpes
655 avenue de l'Europe, 38330 Montbonnot St Martin
URL: http://opera.inrialpes.fr/OPERA
TITRE : Détection d'íncohérences temporelles au sein de
documents multimédia au format SMIL
RESUME :
Le projet Opéra a pour thème général les applications de traitement des
documents électroniques. Un des axes de recherche plus précisément abordé
concerne l'aide à la conception de documents multimédia, en offrant par
exemple des environnements d'édition basés sur différents paradigmes
(contraintes, événements, arbres d'opérateurs).
Par ailleurs, le W3C (consortium mondial regroupant des industriels et des centres de recherche, dont l'objectif est de développer et promouvoir le Web) propose un format de documents multimédia nommé Smil dont la première version a été publiée en Juin 98 [Smil98]. L'objectif de ce format est de permettre l'écriture de documents Web dont les objets sont synchronisés dans le temps. On peut le voir comme une extension du format HTML pour rendre les documents sur le Web plus dynamiques sans pour autant nécessiter de la programmation. Une seconde version du format Smil permettant d'intégrer plus d'intéractivité dans les documents gràce à l'íntégration de la notion d'événements, est en cours de spécification (version finale prévue en décembre 2000 [W3C2000]).
Le risque d'exprimer des incohérences temporelles ("deadlock" potentiel, objets jamais joués, ...) existe dans la première version de ce standard mais est rendu encore plus important dans sa deuxième version par l'íntégration des événements puisque ceux-ci rendent le comportement du document beaucoup moins prévisible statiquement et donc plus difficile à appréhender pour l'auteur. Parallèlement à cela, si comme tout semble l'indiquer, le format Smil devient un format incontournable sur le Web, les exigences des utilisateurs en terme de fiabilité des comportements des documents écrits vont considérablement augmenter.
L'objectif du projet proposé est d'une part d'établir une classification des incohérences temporelles qu'il serait souhaitable de détecter dans la seconde version du format Smil; d'autre part de faire un état de l'art sur les méthodes de vérification formelle susceptibles d'être utilisées (logique temporelle [Boz98], comparaison de graphes [Fer96b], génération de tests [Fer96a, Par96, duB98]. Le résultat de cet état de l'art sera un choix argumenté sur la technique à utiliser, en accordant une place importante à la facilité d'utilisation du processus de détection. Finalement, l'étudiant devra proposer un processus complet plus ou moins automatique de détection des incohérences d'un document Smil, dans lequel l'élaboration du diagnostic d'une incohérence ne devra pas être négligée.
[W3C98] W3C Recommendation Synchronized Multimedia Integration Language (SMIL) 1.0 Specification http://www.w3.org/TR/REC-smil 15-June 1998
[W3C2000] W3C Working draft The Smil Timing and synchronization module http://www.w3.org/AudioVideo/Group/Timing/smil-timing.html
[Fer96a] Jean-Claude Fernandez, Claude Jard, Thierry Jéron, Laurence Nedelka, and César Viho. An experiment in automatic generation of test suites for protocols with verification technology. Science of Computer Programming, 1996. Special issue on Industrially Relevant Applications of Formal Analysis Techniques. Also available as Inria Research Report RR-2923.
[Fer96b] Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Radu Mateescu, Laurent Mounier, and Mihaela Sighireanu. Cadp (cæsar/aldebaran development package): A protocol validation and verification toolbox. In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the 8th Conference on Computer-Aided Verification (New Brunswick, New Jersey, USA), volume 1102 of LNCS, pages 437-440. Springer Verlag, August 1996.
[Boz98] M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: a model-checking tool for real-time systems. In Proc. 10th Conference Computer-Aided Verification, CAV'98,Vancouver, Canada, LNCS. IEEE Computer Society Press, June 1998.
[Par96] I. Parissis and F. Ouabdesselam. Techniques de Test pour des Logiciels Réactifs Synchrones. In Modélisation des Systèmes Réactifs, AFCET, Brest, France, 1996.
[duB98] L. du Bousquet, F. Ouabdesselam, J.-L. Richier, and N. Zuanon. Environnement pour le test d'applications synchrones. In 2ème Congrès sur la Modélisation des systèmes réactifs. Hermes, 1998.
RESULTATS ATTENDUS :
Pratiques (réalisations) :
Conception d'un premier prototype de détection d'incohérences temporelles au sein de documents multimédia au format Smil.
Théoriques :
Identification des incohérences temporelles susceptibles d'être présentes dans un document Smil et classification de ces incohérences.
Choix d'une technique de vérification formelle adaptée au contexte de
l'aide à la conception de documents multimédia.
Automatisation de l'expression des propriétés à vérifier.
Etude des possibilités d'enrichissement du diagnostic fourni par l'outil de vérification en cas d'incohérences.
Mots-clés:
Documents multimédia, standard Smil, vérification formelle, diagnostic