A Mechanized Model for CAN Protocols

Francesco Bongiovanni 1, 2 Ludovic Henrio 3
3 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
Abstract : Formal reasoning on Peer-to-Peer (P2P) systems is an intimidating task. This paper focuses on broadcast algorithms for Content Addressable Network (CAN). Since these algorithms run on top of complex P2P systems, finding the right level of abstraction in order to prove their functional correctness is difficult. This paper presents a mechanized model for both CAN and broadcast protocols over those networks. We demonstrate that our approach is practical by identifying sufficient conditions for a protocol to be correct and efficient. We also prove the existence of a protocol verifying those properties.
Type de document :
Communication dans un congrès
16th International Conference on Fundamental Approaches to Software Engineering (FASE'13), Mar 2013, Rome, Italy. Springer, 2013
Liste complète des métadonnées


https://hal.inria.fr/hal-00802006
Contributeur : Ludovic Henrio <>
Soumis le : lundi 18 mars 2013 - 18:58:02
Dernière modification le : mardi 19 mars 2013 - 08:17:43
Document(s) archivé(s) le : dimanche 2 avril 2017 - 14:38:53

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00802006, version 1

Collections

UNICE | INRIA | LIG | I3S | UGA

Citation

Francesco Bongiovanni, Ludovic Henrio. A Mechanized Model for CAN Protocols. 16th International Conference on Fundamental Approaches to Software Engineering (FASE'13), Mar 2013, Rome, Italy. Springer, 2013. <hal-00802006>

Partager

Métriques

Consultations de
la notice

264

Téléchargements du document

168