Modeling Consensus in a Process Calculus

Abstract. We give a process calculus model that formalizes a wellknown algorithm (introduced by Chandra and Toueg) solving consensus in the presence of a particular class of failure detectors (♦S); we use our model to formally prove that the algorithm satisfies its specification.

• Type: Conference
• Year: 2003
• Where: CONCUR
• Authors: Uwe Nestmann, Rachele Fuzzati, Massimo Merro
• Keywords: CONCUR 2003, Failure Detectors, Process Calculus Model, Wellknown Algorithm