Verifying Safety of Fault-Tolerant Distributed Components -- Extended Version

Rabéa Ameur-Boulifa 1 Raluca Halalai 2 Ludovic Henrio 3 Eric Madelaine 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
Résumé : Nous montrons comment assurer la correction et la tolérance aux pannes de composants distribués à l'aide de spéci cations comportementales. Nous spéci ons un système combinant une application distribuée très simple avec un mécanisme de tolérance aux pannes. Nous avons choisi le type de fautes le plus général et le plus exigeant, les pannes Byzantines, mais seulement pour une partie des composants de notre système. Avec des pannes Byzantines un composant peut avoir n'importe quel comportement, et la replication est la seule solution classique convenable; ceci augmente de beaucoup la taille du système, et sa véri cation par des techniques de model-checking est un dé . Malgré la simplicité de notre application, l' étude complète du système nous oblige à combiner de nombreux aspects nécessaires à l'application distibuée ou au protocole de tolérance aux pannes: notre système utilise une architecture de composants hiérarchiques, des communications asynchrones avec futurs, de la replication, de la communication de groupe, et un protocole de consensus. Le système obtenu est très gros, et nous avons pouvé sa correction en combinant des techniques d'abstraction de données, de minimisation compositionnelle, et de model-checking distribué.
Type de document :
Rapport
[Research Report] RR-7717, INRIA. 2011, pp.31
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00621264
Contributeur : Eric Madelaine <>
Soumis le : mardi 13 septembre 2011 - 08:54:22
Dernière modification le : mardi 12 juin 2018 - 10:04:04
Document(s) archivé(s) le : mardi 13 novembre 2012 - 10:35:46

Fichier

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

Identifiants

  • HAL Id : inria-00621264, version 1

Collections

Citation

Rabéa Ameur-Boulifa, Raluca Halalai, Ludovic Henrio, Eric Madelaine. Verifying Safety of Fault-Tolerant Distributed Components -- Extended Version. [Research Report] RR-7717, INRIA. 2011, pp.31. 〈inria-00621264〉

Partager

Métriques

Consultations de la notice

632

Téléchargements de fichiers

318