Abstract
We give a process calculus model that formalizes a well-known algorithm (introduced by Chandra and Toueg) solving consensus in the presence of a particular class of failure detectors (\(\diamondsuit \mathcal{S}\)); we use our model to formally prove that the algorithm satisfies its specification.
Supported by the Swiss National Science Foundation, grant No. 21-67715.02, the Hasler Foundation, grant No. DICS 1825, an EPFL start-up grant, and the EU FET-GC project PEPITO. The full version is available at: http://lamp.epfl.ch/~uwe/
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Berger, M., Honda, K.: The Two-Phase Commitment Protocol in an Extended pi-Calculus. In: Aceto, L., Victor, B. (eds.) Proceedings of EXPRESS 2000. ENTCS, vol. 39.1. Elsevier Science Publishers, Amsterdam (2000)
Chandra, T.D., Hadzilacos, V., Toueg, S.: The Weakest Failure Detector for Solving Consensus. Journal of the ACM 43(4), 685–722 (1996)
Chandra, T.D., Toueg, S.: Unreliable Failure Detectors for Reliable Distributed Systems. Journal of the ACM 43(2), 225–267 (1996)
Fisher, M.J., Lynch, N., Patterson, M.: Impossibility of Distributed Concensus with One Faulty Process. Journal of the ACM 32(2), 374–382 (1985)
Pogosyants, A., Segala, R., Lynch, N.: Verification of the Randomized Consensus Algorithm of Aspnes and Herlihy: a Case Study. Distributed Computing 13(3), 155–186 (2000)
Riely, J., Hennessy, M.: Distributed Processes and Location Failures. Theoretical Computer Science 226, 693–735 (2001)
Wojciechowski, P., Sewell, P.: Nomadic Pict: Language and Infrastructure Design for Mobile Agents. IEEE Concurrency 8(2), 42–52 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nestmann, U., Fuzzati, R., Merro, M. (2003). Modeling Consensus in a Process Calculus. In: Amadio, R., Lugiez, D. (eds) CONCUR 2003 - Concurrency Theory. CONCUR 2003. Lecture Notes in Computer Science, vol 2761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45187-7_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-45187-7_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40753-9
Online ISBN: 978-3-540-45187-7
eBook Packages: Springer Book Archive