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
Abstract : We shows how to ensure correctness and fault-tolerance of distributed components by behavioural speci cation. We specify a system combining a simple distributed component application and a fault-tolerance mechanism. We choose to encode the most general and the most demanding kind of faults, Byzantine failures, but only for some of the components of our system. With Byzantine failures a faulty process can have any behaviour, thus replication is the only convenient classical solution; this greatly increases the size of the system, and makes model-checking a challenge. Despite the simplicity of our application, full study of the overall behaviour of the combined system requires us putting together the speci cation for many features required by either the distributed application or the fault-tolerant protocol: our system encodes hierarchical component structure, asynchronous communication with futures, replication, group communication, an agreement protocol, and faulty components. The system we obtain is huge and we have proved its correctness by using at the same time data abstraction, compositional minimization, and distributed model-checking.
Document type :
Reports
[Research Report] RR-7717, INRIA. 2011, pp.31
Liste complète des métadonnées

Cited literature [2 references]  Display  Hide  Download

https://hal.inria.fr/inria-00621264
Contributor : Eric Madelaine <>
Submitted on : Tuesday, September 13, 2011 - 8:54:22 AM
Last modification on : Wednesday, January 31, 2018 - 10:24:04 AM
Document(s) archivé(s) le : Tuesday, November 13, 2012 - 10:35:46 AM

File

RR7717.pdf
Files produced by the author(s)

Identifiers

  • 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〉

Share

Metrics

Record views

599

Files downloads

307