Le protocole Pastry réalise une table de hachage distribué sur un réseau pair à pair organisé en un anneau virtuel de noeuds. Alors qu'il existe plusieurs implémentations de Pastry, il n'y a pas encore eu de travaux pour décrire formellement l'algorithme ou vérifier son bon fonctionnement. Intégrant des structures de données complexes et de la communication asynchrone entre des noeuds qui peuvent rejoindre ou quitter le réseau, ce protocole représente un intérêt certain pour la vérification formelle. La thèse se focalise sur le protocole Join de Pastry qui permet à un noeud de rejoindre le réseau. Les noeuds ayant intégré le réseau doivent avoir une vue du voisinage cohérente entre eux. La propriété principale de correction, appelée CorrectDelivery, assure qu'à tout moment il y a au plus un noeud capable de répondre à une requête pour une clé, et que ce noeud est le noeud le plus proche numériquement à ladite clé. Il n'est pas trivial de maintenir cette propriété en présence de churn. Ce travail nous a permis de découvrir des violations inattendues de la propriété dans les versions publiées de l'algorithme. Sur la base de cette analyse, le protocole IdealPastry est conçu et vérifié en utilisant l'assistant interactif à la preuve TLAPS pour TLA+. Le protocole LuPastry est obtenu en assouplissant certaines hypothèses de IdealPastry. Il est montré formellement que LuPastry vérifie CorrectDelivery sous l'hypothèse qu'aucun noeud ne quitte le réseau. Cette hypothèse ne peut être relâchée à cause du risque de perte de connexion du réseau dans le cas où plusieurs noeuds quittent le réseau en même temps / Pastry is a structured P2P algorithm realizing a Distributed Hash Table over an underlying virtual ring of nodes. Several implementations of Pastry are available, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines complex data structures, asynchronous communication, and concurrency in the presence of spontaneous join and departure of nodes, it makes an interesting target for verification. This thesis focuses on the Join protocol of Pastry that integrates new nodes into the ring. All member nodes must have a consistent key mapping among each other. The main correctness property, named CorrectDelivery, states that there is always at most one node that can deliver an answer to a lookup request for a key and this node is the numerically closest member node to that key. This property is non-trivial to preserve in the presence of churn. In this thesis, unexpected violations of CorrectDelivery in the published versions of Pastry are discovered and analyzed using the TLA+ model checker TLC. Based on the analysis, the protocol IdealPastry is designed and verified using the interactive theorem prover TLAPS for TLA+. By relaxing certain hypotheses, IdealPastry is further improved to LuPastry, which is again formally proved correct under the assumption that no nodes leave the network. This hypothesis cannot be relaxed in general due to possible network separation when particular nodes simultaneously leave the network

Au cours de la dernière décennie, nous avons assisté à une croissance exponentielle de documents numériques et de ressources multimédias, y compris une présence massive de ressources vidéo. Les vidéos sont devenu de plus en plus populaire grâce au contenue riche à l'audio riche qu'elles véhiculent (contenu audiovisuelle et textuelle). Les dernières avancées technologiques ont rendu disponibles aux utilisateurs cette grande quantité de ressources multimédias et cela dans une variété de domaines, y compris les domaines académiques et scientifiques. Toutefois, sans techniques adéquates se basant sur le contenu des multimédia, cette masse de donnée précieuse est difficilement accessible et demeure en vigueur inutilisable. Cette thèse explore les approches sémantiques pour la gestion ainsi que la navigation et la visualisation des ressources multimédias générées par les conférences scientifiques. Un écart, que l'on appelle sémantique, existe entre la représentation des connaissances explicites requis par les utilisateurs qui cherchent des ressources multimédias et la connaissance implicite véhiculée le long du cycle de vie d'une conférence. Le but de ce travail est de fournir aux utilisateurs une plateforme qui améliore la recherche de l'information multimédia des conférences en diminuant cette distance sémantique. L'objectif de cette thèse est de fournir une nouvelle approche pour le contenu multimédia basé sur la recherche d'information dans le domaine des conférences scientifiques.

Avec l'évolution des réseaux fixes et mobiles, des terminaux de plus en plus nombreux et diversifiés, il est maintenant possible d'accéder à n'importe quel type de service, depuis n'importe quel type de terminal, en étant connecté sur n'importe quel type de réseau. En ajoutant le souhait des utilisateurs de recevoir un contenu personnalisé, l'adaptation de contenu est devenue une problématique majeure. Cette thèse définit une solution de noeud intermédiaire, flexible permettant l'adaptation dynamique de tout type de contenu en fonction du contexte de l'utilisateur. Ces travaux ont abouti à la définition d'une architecture de noeud, dénommé Potacco pour noeud POlymorphique Transparent pour l'Adaptation de Contenu adapté au COntexte, à sa mise en oeuvre et sa validation. Ce noeud : * collecte et met à disposition le contexte courant pour permettre aux modules applicatifs de réaliser des adaptations en fonction de ces valeurs * gère/coordonne les modules applicatifs et les collecteurs de contexte * permet le déploiement sécurisé de code dans le noeud avec authentification du fournisseur du code, mais aussi du noeud cible * peut être transparent en réalisant des traitements sans que les points terminaux puissent s'en apercevoir. Deux démonstrateurs constituent une preuve de concept de ce noeud générique, intégré dans un réseau physique: une passerelle filaire/sans-fil réalisant l'adaptation de contenu média et un noeud dans un réseau ADSL insérant dynamiquement le contexte des utilisateurs. Ensuite, l'apport de ce noeud dans le cadre des réseaux "overlays" a fait l'objet d'une nouvelle preuve de concept. Deux cas ont été étudiés: la première pour la fourniture de service adapté au contexte de l'utilisateur dans un réseau overlay de service, où un cas d'usage de service d'IPTV personnalisé est présenté; la deuxième relative à l'adaptation de contenu de flux multimédia diffusé sur un réseau P2P où le noeud Potacco est lui-même membre du réseau P2P. Des évaluations, par simulation et expérimentation réelle, ont permis d'évaluer ces solutions.