Abstract
We exhibit a methodology to develop mechanically-checkable parameterized proofs of the correctness of fault-tolerant round-based distributed algorithms in an asynchronous message-passing setting. Motivated by a number of case studies, we sketch how to replace often-used informal and incomplete pseudo code by mostly syntax-free formal and complete definitions of a global-state transition system. Special emphasis is put on the required deepening of the level of proof detail to be able to check them within an interactive theorem proving environment.
Chapter PDF
Similar content being viewed by others
References
Ballarin, C.: Locales and Locale Expressions in Isabelle/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 34–50. Springer, Heidelberg (2004)
Charron-Bost, B., Debrat, H., Merz, S.: Formal Verification of Consensus Algorithms Tolerating Malicious Faults. In: Défago, X., Petit, F., Villain, V. (eds.) SSS 2011. LNCS, vol. 6976, pp. 120–134. Springer, Heidelberg (2011)
Clarke, E.M.: Proving the correctness of coroutines without history variables. In: ACM-SE 16, pp. 160–167. ACM, New York (1978)
Clint, M.: Program proving: Coroutines. Acta Informatica 2, 50–63 (1973)
Clint, M.: On the use of history variables. Acta Informatica 16, 15–30 (1981)
Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. Journal of the ACM 43, 225–267 (1996)
Francalanza, A., Hennessy, M.: A Fault Tolerance Bisimulation Proof for Consensus (Extended Abstract). In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 395–410. Springer, Heidelberg (2007)
Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374–382 (1985)
Fuzzati, R., Merro, M., Nestmann, U.: Distributed Consensus, Revisited. Acta Informatica 44(6), 377–425 (2007)
Fuzzati, R.: A Formal Approach to Fault Tolerant Distributed Consensus. PhD thesis, EPFL, Lausanne (2008)
Gafni, E., Lamport, L.: Disk Paxos. In: Herlihy, M.P. (ed.) DISC 2000. LNCS, vol. 1914, pp. 330–344. Springer, Heidelberg (2000)
Gurevich, Y.: Evolving algebras: An attempt to discover semantics (1993)
Jaskelioff, M., Merz, S.: Proving the correctness of disk paxos. In: The Archive of Formal Proofs (2005), http://afp.sf.net/entries/DiskPaxos.shtml
Lamport, L.: The implementation of reliable distributed multiprocess systems. Computer Networks 2(2), 95–114 (1976)
Lamport, L.: The part-time parliament. ACM Transactions on Computer Systems 16, 133–169 (1998)
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)
Lamport, L., Shostak, R., Pease, M.: The byzantine generals problem. ACM ToPLaS 4(3), 382–401 (1982)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Pub. (1996)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Owicki, S.: A consistent and complete deductive system for the verification of parallel programs. In: Proceedings of STOC 1976, pp. 73–86. ACM (1976)
Schneider, F.B.: Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys 22, 299–319 (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Küfner, P., Nestmann, U., Rickmann, C. (2012). Formal Verification of Distributed Algorithms. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds) Theoretical Computer Science. TCS 2012. Lecture Notes in Computer Science, vol 7604. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33475-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-33475-7_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33474-0
Online ISBN: 978-3-642-33475-7
eBook Packages: Computer ScienceComputer Science (R0)