Formalising replicated distributed processing

The authors present a novel formal approach to proving the correctness of distributed systems of replicated processes that communicate by message passing. The notion of correctness introduced is based on the consistency of the replicated system with its nonreplicated counterpart. The formal framework of CSP (communicating sequential processes) allows the proof of partial correctness and deadlock-freedom properties of the systems of replicated processes. The authors also discuss how a replicated process may be implemented by N-base copies, a majority of which are non-faulty, and point out the necessity of coordinating the copies and the requirements they should satisfy.<>