Skip to Main content Skip to Navigation

A Fault Tolerance protocol for ASP calculus: Design and Proof

Françoise Baude 1 Denis Caromel 1 Christian Delbé 1 Ludovic Henrio 1
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : This research report first details a communication induced checkpointing fault tolerance protocol adapted to ProActive, a Java library that implements the ASP model. This model is based n a request/reply mechanism. In order to prove the correctness of this protocol, we introduce a local partial order between events occurring on a given process. This order is extended into a global order by the Lamport's happened-before relation. Finally, we prove that from a cut that is ''consistent enough'', a second execution is constrained to go equivalently to the first one until a consistent global state of the first one (the history closure). Thus, the protocol described in this report ensures that, even from a inconsistent recovery line, a reexecution cannot lead to an inconsistent state that could not exist in a normal execution.
Document type :
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 9:30:39 PM
Last modification on : Friday, February 4, 2022 - 3:18:16 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:05:56 PM


  • HAL Id : inria-00070752, version 1



Françoise Baude, Denis Caromel, Christian Delbé, Ludovic Henrio. A Fault Tolerance protocol for ASP calculus: Design and Proof. [Research Report] RR-5246, INRIA. 2004, pp.37. ⟨inria-00070752⟩



Record views


Files downloads