Mechanical Support for Efficient Dissemination on the CAN Overlay Network

Francesco Bongiovanni 1 Ludovic Henrio 1
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Résumé : Les différents algorithmes sous-jacents des systèmes Pair-à-Pair sont notoirement difficiles à concevoir et à analyser. Créer de nouveaux algorithmes prouvés corrects pour de tels systèmes à grande échelle est une tâche difficile. Nous rapportons les premières étapes d'un travail en cours qui vise à concevoir un algorithme de diffusion qui est correct par construction et efficace pour le réseau de recouvrement structuré CAN. Afin de raisonner de manière rigoureuse sur un tel algorithme et d'en prouver son exactitude nous nous appuyons sur un assistant de preuve interactif: Isabelle / HOL. Cet article présente un cadre de raisonnement générique qui devrait faciliter la promotion de preuves de correction formelle d'algorithmes de multicast existants et de faciliter la conception de nouveaux algorithmes.
Type de document :
Rapport
[Research Report] RR-7599, INRIA. 2011
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00585057
Contributeur : Francesco Bongiovanni <>
Soumis le : mercredi 13 avril 2011 - 10:41:53
Dernière modification le : jeudi 11 janvier 2018 - 15:59:52
Document(s) archivé(s) le : jeudi 8 novembre 2012 - 16:15:18

Fichier

RR-7599.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00585057, version 1

Collections

Citation

Francesco Bongiovanni, Ludovic Henrio. Mechanical Support for Efficient Dissemination on the CAN Overlay Network. [Research Report] RR-7599, INRIA. 2011. 〈inria-00585057〉

Partager

Métriques

Consultations de la notice

363

Téléchargements de fichiers

178