Abstract FR:

La complexite temporelle, logique et semantique des systemes multimedias et hypermedias rend necessaire l'utilisation de techniques formelles permettant de specifier ces systemes et de verifier, en prealable a leur conception, leurs proprietes logiques et temporelles. Cette these introduit une nouvelle technique de modelisation de systemes multimedias et hypermedias basee sur le formalisme des reseaux de petri etendus par le temps. Ce modele appele reseaux de petri a flux temporels (rdpft) permet de specifier l'indeterminisme temporel intrinseque aux systemes distribues multimedias en associant un intervalle temporel aux arcs sortant des places d'un reseau de petri. Les rdpft introduisent de plus une semantique formelle de la synchronisation en environnement faiblement synchrone. Cette semantique formelle, definie a l'aide de 9 types de regles de tir pouvant etre selectivement associees aux transitions d'un rdpft, permet de maitriser l'indeterminisme de synchronisation introduit par la variabilite temporelle des traitements. Ainsi, les rdpft permettent de modeliser de facon complete, precise et aisee les contraintes de synchronisation des systemes multimedias. Cette these considere egalement la classe des rdpft construits a l'aide des operateurs de l'algebre temporelle de allen. Cette classe, appelee reseaux de petri structures a flux temporels (rdpsft), permet une verification aisee des proprietes temporelles d'un systeme multimedia et offre de plus des bases formelles pour la representation abstraite des structures logiques et temporelles d'un systeme multimedia. Finalement cette these introduit une extension des rdpft, appelee reseaux de petri hierarchises a flux temporels (rdphft). Cette extension, beneficiant de tous les acquis theoriques des rdpft, permet de modeliser a l'aide d'un formalisme unificateur les composants d'un systeme hypermedia et introduit une semantique formelle de la notion de synchronisation hypermedia. De plus les rdphft offrent un support methodologique permettant une specification modulaire et hierarchisee des systemes hypermedias, et plus generalement des systemes a contraintes temporelles