Modelling and Verification of a Checkpoint-Restart-Protocol

Abstract

The paper presents a protocol for the treatment of temporary local crashes and communication failures in systems of communicating processes. Assuming the existence of a global partitioning of the processes’ interactions into a sequence of segments as well as the availability of a reliable memory to each participant, the recovery strategy lies in the provident permanent recording and discarding of checkpoint data and, in cases of failure, common restarts from some recent global checkpoint (boundary between two segments). Apart from the inherent limitations imposed by data flow and resources the processes may run totally asynchronously. The protocol is modelled by a PrT-net, which permits to formally state and verify the protocol’s service, namely guaranteeing liveness and the eventual progress of the system’s actions. The final part of this paper is devoted to the structure and basic ideas of this proof.