Advertisement

Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms

  • Annu Gmeiner
  • Igor Konnov
  • Ulrich Schmid
  • Helmut Veith
  • Josef Widder
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8483)

Abstract

Recently we introduced an abstraction method for parameterized model checking of threshold-based fault-tolerant distributed algorithms. We showed how to verify distributed algorithms without fixing the size of the system a priori. As is the case for many other published abstraction techniques, transferring the theory into a running tool is a challenge. It requires understanding of several verification techniques such as parametric data and counter abstraction, finite state model checking and abstraction refinement. In the resulting framework, all these techniques should interact in order to achieve a possibly high degree of automation. In this tutorial we use the core of a fault-tolerant distributed broadcasting algorithm as a case study to explain the concepts of our abstraction techniques, and discuss how they can be implemented.

Keywords

Model Check Correct Process Abstract Domain Spurious Transition Concrete System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    ByMC 0.4.0: Byzantine model checker (2013), http://forsyte.tuwien.ac.at/software/bymc/ (accessed March 2014)
  2. 2.
    Spin 6.2.7 (2014), http://spinroot.com/ (accessed March 2014)
  3. 3.
    Tempo toolset. Web page, http://www.veromodo.com/
  4. 4.
    TLA – the temporal logic of actions. Web page, http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html
  5. 5.
    Yices 1.0.40 (2013), http://yices.csl.sri.com/yices1-documentation.shtml (accessed March 2014)
  6. 6.
    Abdulla, P.A.: Regular model checking. International Journal on Software Tools for Technology Transfer 14, 109–118 (2012)CrossRefGoogle Scholar
  7. 7.
    Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput. 127(2), 91–101 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Aguilera, M.K., Delporte-Gallet, C., Fauconnier, H., Toueg, S.: Consensus with Byzantine failures and little system synchrony. In: DSN, pp. 147–155 (2006)Google Scholar
  9. 9.
    Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Universal guards, relativization of quantifiers, and failure models in model checking modulo theories. JSAT 8(1/2), 29–61 (2012)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 15, 307–309 (1986)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Attiya, H., Welch, J.: Distributed Computing, 2nd edn. John Wiley & Sons (2004)Google Scholar
  12. 12.
    Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press (2008)Google Scholar
  13. 13.
    Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of c programs. In: PLDI, pp. 203–213 (2001)Google Scholar
  14. 14.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal 4.0 (2006)Google Scholar
  15. 15.
    Biely, M., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A., Widder, J.: Tolerating corrupted communication. In: PODC, pp. 244–253 (August 2007)Google Scholar
  16. 16.
    Biely, M., Schmid, U., Weiss, B.: Synchronous consensus under hybrid process and link failures. Theoretical Computer Science 412(40), 5602–5630 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Biere, A.: Handbook of satisfiability, vol. 185. IOS Press (2009)Google Scholar
  18. 18.
    Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: DAC, pp. 317–320 (1999)Google Scholar
  19. 19.
    Bokor, P., Kinder, J., Serafini, M., Suri, N.: Efficient model checking of fault-tolerant distributed protocols. In: DSN, pp. 73–84 (2011)Google Scholar
  20. 20.
    Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM 32(4), 824–840 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81, 13–31 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Chambart, P., Schnoebelen, P.: Mixing lossy and perfect fifo channels. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 340–355. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225–267 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    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)CrossRefGoogle Scholar
  25. 25.
    Charron-Bost, B., Pedone, F., Schiper, A. (eds.): Replication: Theory and Practice. LNCS, vol. 5959. Springer, Heidelberg (2010)Google Scholar
  26. 26.
    Chou, C.T., Mannava, P., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382–398. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  27. 27.
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Clarke, E., Talupur, M., Veith, H.: Proving Ptolemy right: the environment abstraction framework for model checking concurrent systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 33–47. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  29. 29.
    Clarke, E., Talupur, M., Touili, T., Veith, H.: Verification by network decomposition. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 276–291. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  30. 30.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  31. 31.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)Google Scholar
  32. 32.
    Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 126–141. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  33. 33.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252. ACM (1977)Google Scholar
  34. 34.
    Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)CrossRefGoogle Scholar
  35. 35.
    de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  36. 36.
    De Prisco, R., Malkhi, D., Reiter, M.K.: On k-set consensus problems in asynchronous systems. IEEE Trans. Parallel Distrib. Syst. 12(1), 7–21 (2001)CrossRefzbMATHGoogle Scholar
  37. 37.
    Dolev, D., Lynch, N.A., Pinter, S.S., Stark, E.W., Weihl, W.E.: Reaching approximate agreement in the presence of faults. J. ACM 33(3), 499–516 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  39. 39.
    Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. J. ACM 35(2), 288–323 (1988)MathSciNetCrossRefGoogle Scholar
  40. 40.
    Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 236–254. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  41. 41.
    Emerson, E., Namjoshi, K.: Reasoning about rings. In: POPL, pp. 85–94 (1995)Google Scholar
  42. 42.
    Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374–382 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  43. 43.
    Fisman, D., Kupferman, O., Lustig, Y.: On verifying fault tolerance of distributed protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 315–331. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  44. 44.
    Fuegger, M., Schmid, U., Fuchs, G., Kempf, G.: Fault-Tolerant Distributed Clock Generation in VLSI Systems-on-Chip. In: EDCC 2006, pp. 87–96 (October 2006)Google Scholar
  45. 45.
    German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39, 675–735 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  46. 46.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  47. 47.
    Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol. 5000. Springer, Heidelberg (2008)zbMATHGoogle Scholar
  48. 48.
    Halbwachs, N., Lagnier, F., Ratel, C.: Programming and verifying real-time systems by means of the synchronous data-flow language lustre. IEEE Trans. Softw. Eng. 18, 785–793 (1992)CrossRefzbMATHGoogle Scholar
  49. 49.
    Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional (2003)Google Scholar
  50. 50.
    Ip, C., Dill, D.: Verifying systems with replicated components in murφ. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 147–158. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  51. 51.
    John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Starting a dialog between model checking and fault-tolerant distributed algorithms. arXiv CoRR abs/1210.3839 (2012)Google Scholar
  52. 52.
    John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: FMCAD, pp. 201–209 (2013)Google Scholar
  53. 53.
    John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 209–226. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  54. 54.
    Joshi, R., Lamport, L., Matthews, J., Tasiran, S., Tuttle, M.R., Yu, Y.: Checking cache-coherence protocols with TLA + . Formal Methods in System Design 22(2), 125–131 (2003)CrossRefzbMATHGoogle Scholar
  55. 55.
    Kaynar, D.K., Lynch, N.A., Segala, R., Vaandrager, F.W.: The Theory of Timed I/O Automata. Synthesis Lectures on Computer Science. Morgan & Claypool (2006)Google Scholar
  56. 56.
    Kesten, Y., Pnueli, A.: Control and data abstraction: the cornerstones of practical formal verification. STTT 2, 328–342 (2000)CrossRefzbMATHGoogle Scholar
  57. 57.
    Konnov, I., Veith, H., Widder, J.: Who is afraid of Model Checking Distributed Algorithms? (2012)Google Scholar
  58. 58.
    Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16, 133–169 (1998)CrossRefGoogle Scholar
  59. 59.
    Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)Google Scholar
  60. 60.
    Lamport, L.: The pluscal algorithm language. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 36–60. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  61. 61.
    Lincoln, P., Rushby, J.: A formally verified algorithm for interactive consistency under a hybrid fault model. In: FTCS-23, pp. 402–411 (June 1993)Google Scholar
  62. 62.
    Lynch, N.: Distributed Algorithms. Morgan Kaufman, San Francisco (1996)Google Scholar
  63. 63.
    Lynch, N., Tuttle, M.: An introduction to input/output automata. Tech. Rep. MIT/LCS/TM-373, Laboratory for Computer Science, MIT (1989)Google Scholar
  64. 64.
    McMillan, K.: Symbolic model checking. Kluwer (1993)Google Scholar
  65. 65.
    McMillan, K.L.: Parameterized verification of the flash cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 179–195. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  66. 66.
    Mitra, S., Lynch, N.A.: Proving approximate implementations for probabilistic I/O automata. Electr. Notes Theor. Comput. Sci. 174(8), 71–93 (2007)CrossRefzbMATHGoogle Scholar
  67. 67.
    Mostéfaoui, A., Mourgaya, E., Parvédy, P.R., Raynal, M.: Evaluating the condition-based approach to solve consensus. In: DSN, pp. 541–550 (2003)Google Scholar
  68. 68.
    O’Leary, J.W., Talupur, M., Tuttle, M.R.: Protocol verification using flows: An industrial experience. In: FMCAD, pp. 172–179 (2009)Google Scholar
  69. 69.
    Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. J. ACM 27(2), 228–234 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
  70. 70.
    Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0,1, ∞ )-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–111. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  71. 71.
    Powell, D.: Failure mode assumptions and assumption coverage. In: FTCS-22, Boston, MA, USA, pp. 386–395 (1992)Google Scholar
  72. 72.
    Santoro, N., Widmayer, P.: Time is not a healer. In: Cori, R., Monien, B. (eds.) STACS 1989. LNCS, vol. 349, pp. 304–313. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  73. 73.
    Schmid, U., Weiss, B., Rushby, J.: Formally verified Byzantine agreement in presence of link faults. In: ICDCS, July 2-5, pp. 608–616 (2002)Google Scholar
  74. 74.
    Shoham, S., Grumberg, O.: 3-valued abstraction: More precision at less cost. Inf. Comput. 206(11), 1313–1333 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  75. 75.
    Srikanth, T.K., Toueg, S.: Optimal clock synchronization. Journal of the ACM 34(3), 626–645 (1987)MathSciNetCrossRefGoogle Scholar
  76. 76.
    Srikanth, T., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distributed Computing 2, 80–94 (1987)CrossRefGoogle Scholar
  77. 77.
    Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213–214 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  78. 78.
    Tsuchiya, T., Schiper, A.: Verification of consensus algorithms using satisfiability solving. Distributed Computing 23(5-6), 341–358 (2011)CrossRefzbMATHGoogle Scholar
  79. 79.
    Widder, J., Biely, M., Gridling, G., Weiss, B., Blanquart, J.P.: Consensus in the presence of mortal Byzantine faulty processes. Distributed Computing 24(6), 299–321 (2012)CrossRefzbMATHGoogle Scholar
  80. 80.
    Widder, J., Schmid, U.: Booting clock synchronization in partially synchronous systems with hybrid process and link failures. Distributed Computing 20(2), 115–140 (2007)CrossRefzbMATHGoogle Scholar
  81. 81.
    Wöhrle, S., Thomas, W.: Model checking synchronized products of infinite transition systems. LMCS 3(4) (2007)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Annu Gmeiner
    • 1
  • Igor Konnov
    • 1
  • Ulrich Schmid
    • 1
  • Helmut Veith
    • 1
  • Josef Widder
    • 1
  1. 1.Vienna University of Technology (TU Wien)Austria

Personalised recommendations