Article

Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms

Authors:

Josef WidderAuthors Info & Claims

Advanced Lectures of the 14th International School on Formal Methods for Executable Software Models - Volume 8483

Pages 122 - 171

https://doi.org/10.1007/978-3-319-07317-0_4

Published: 16 June 2014 Publication History

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.

References

[1]

ByMC 0.4.0: Byzantine model checker 2013, http://forsyte.tuwien.ac.at/software/bymc/ accessed March 2014

[2]

Spin 6.2.7 2014, http://spinroot.com/ accessed March 2014

[3]

Tempo toolset. Web page, http://www.veromodo.com/

[4]

TLA --- the temporal logic of actions. Web page, http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html

[5]

Yices 1.0.40 2013, http://yices.csl.sri.com/yices1-documentation.shtml accessed March 2014

[6]

Abdulla, P.A.: Regular model checking. International Journal on Software Tools for Technology Transfer 14, 109---118 2012

Digital Library

[7]

Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput. 1272, 91---101 1996

Digital Library

[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

Digital Library

[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 81/2, 29---61 2012

[10]

Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 15, 307---309 1986

Digital Library

[11]

Attiya, H., Welch, J.: Distributed Computing, 2nd edn. John Wiley & Sons 2004

[12]

Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press 2008

Digital Library

[13]

Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of c programs. In: PLDI, pp. 203---213 2001

Digital Library

[14]

Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal 4.0 2006

[15]

Biely, M., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A., Widder, J.: Tolerating corrupted communication. In: PODC, pp. 244---253 August 2007

Digital Library

[16]

Biely, M., Schmid, U., Weiss, B.: Synchronous consensus under hybrid process and link failures. Theoretical Computer Science 41240, 5602---5630 2011

Digital Library

[17]

Biere, A.: Handbook of satisfiability, vol. 185. IOS Press 2009

Digital Library

[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

Digital Library

[19]

Bokor, P., Kinder, J., Serafini, M., Suri, N.: Efficient model checking of fault-tolerant distributed protocols. In: DSN, pp. 73---84 2011

Digital Library

[20]

Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM 324, 824---840 1985

Digital Library

[21]

Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81, 13---31 1989

Digital Library

[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

Digital Library

[23]

Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 432, 225---267 1996

Digital Library

[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

Digital Library

[25]

Charron-Bost, B., Pedone, F., Schiper, A. eds.: Replication: Theory and Practice. LNCS, vol. 5959. Springer, Heidelberg 2010

Digital Library

[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

[27]

Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 505, 752---794 2003

Digital Library

[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

Digital Library

[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

[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

Digital Library

[31]

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press 1999

Digital Library

[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

Digital Library

[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

Digital Library

[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. 134, 451---490 1991

Digital Library

[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

Digital Library

[36]

De Prisco, R., Malkhi, D., Reiter, M.K.: On k-set consensus problems in asynchronous systems. IEEE Trans. Parallel Distrib. Syst. 121, 7---21 2001

Digital Library

[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 333, 499---516 1986

Digital Library

[38]

Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLLT. In: Ball, T., Jones, R.B. eds. CAV 2006. LNCS, vol. 4144, pp. 81---94. Springer, Heidelberg 2006

Digital Library

[39]

Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. J. ACM 352, 288---323 1988

Digital Library

[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

Digital Library

[41]

Emerson, E., Namjoshi, K.: Reasoning about rings. In: POPL, pp. 85---94 1995

Digital Library

[42]

Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 322, 374---382 1985

Digital Library

[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

Digital Library

[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

Digital Library

[45]

German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39, 675---735 1992

Digital Library

[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

Digital Library

[47]

Grumberg, O., Veith, H. eds.: 25 Years of Model Checking. LNCS, vol. 5000. Springer, Heidelberg 2008

[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

Digital Library

[49]

Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional 2003

Digital Library

[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

Digital Library

[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

[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

[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

[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 222, 125---131 2003

Digital Library

[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

Digital Library

[56]

Kesten, Y., Pnueli, A.: Control and data abstraction: the cornerstones of practical formal verification. STTT 2, 328---342 2000

[57]

Konnov, I., Veith, H., Widder, J.: Who is afraid of Model Checking Distributed Algorithms? 2012

[58]

Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16, 133---169 1998

Digital Library

[59]

Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley 2002

Digital Library

[60]

Lamport, L.: The pluscal algorithm language. In: Leucker, M., Morgan, C. eds. ICTAC 2009. LNCS, vol. 5684, pp. 36---60. Springer, Heidelberg 2009

Digital Library

[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

[62]

Lynch, N.: Distributed Algorithms. Morgan Kaufman, San Francisco 1996

Digital Library

[63]

Lynch, N., Tuttle, M.: An introduction to input/output automata. Tech. Rep. MIT/LCS/TM-373, Laboratory for Computer Science, MIT 1989

[64]

McMillan, K.: Symbolic model checking. Kluwer 1993

Digital Library

[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

Digital Library

[66]

Mitra, S., Lynch, N.A.: Proving approximate implementations for probabilistic I/O automata. Electr. Notes Theor. Comput. Sci. 1748, 71---93 2007

Digital Library

[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

[68]

O'Leary, J.W., Talupur, M., Tuttle, M.R.: Protocol verification using flows: An industrial experience. In: FMCAD, pp. 172---179 2009

[69]

Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. J. ACM 272, 228---234 1980

Digital Library

[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

Digital Library

[71]

Powell, D.: Failure mode assumptions and assumption coverage. In: FTCS-22, Boston, MA, USA, pp. 386---395 1992

[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

Digital Library

[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

Digital Library

[74]

Shoham, S., Grumberg, O.: 3-valued abstraction: More precision at less cost. Inf. Comput. 20611, 1313---1333 2008

Digital Library

[75]

Srikanth, T.K., Toueg, S.: Optimal clock synchronization. Journal of the ACM 343, 626---645 1987

Digital Library

[76]

Srikanth, T., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distributed Computing 2, 80---94 1987

Digital Library

[77]

Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 284, 213---214 1988

Digital Library

[78]

Tsuchiya, T., Schiper, A.: Verification of consensus algorithms using satisfiability solving. Distributed Computing 235-6, 341---358 2011

Digital Library

[79]

Widder, J., Biely, M., Gridling, G., Weiss, B., Blanquart, J.P.: Consensus in the presence of mortal Byzantine faulty processes. Distributed Computing 246, 299---321 2012

Digital Library

[80]

Widder, J., Schmid, U.: Booting clock synchronization in partially synchronous systems with hybrid process and link failures. Distributed Computing 202, 115---140 2007

Digital Library

[81]

Wöhrle, S., Thomas, W.: Model checking synchronized products of infinite transition systems. LMCS 34 2007

Cited By

Aminof BKotek TRubin SSpegni FVeith H(2018)Parameterized model checking of rendezvous systemsDistributed Computing10.1007/s00446-017-0302-631:3(187-222)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s00446-017-0302-6
Konnov ILazić MVeith HWidder J(2017)A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsACM SIGPLAN Notices10.1145/3093333.300986052:1(719-734)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009860
Konnov ILazić MVeith HWidder JCastagna GGordon A(2017)A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009860(719-734)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009860
Show More Cited By

Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms

Recommendations

Language and Tool Support for Model Checking of Fault-Tolerant Distributed Algorithms
PRDC '08: Proceedings of the 2008 14th IEEE Pacific Rim International Symposium on Dependable Computing

Model checking is a successful formal verification technique; however, its application to fault-tolerant distributed algorithms is still not common practice. One major reason for this is that model checking requires non-negligible users’ efforts in ...
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
POPL '17

Distributed algorithms have many mission-critical applications ranging from embedded systems and replicated databases to cloud computing. Due to asynchronous communication, process faults, or network failures, these algorithms are difficult to design ...
Parameterised three-valued model checking

Three-valued abstraction is an established technique in software model checking. It proceeds by generating a state space model over the values true, false and unknown, where the latter value is used to represent the loss of information due to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Advanced Lectures of the 14th International School on Formal Methods for Executable Software Models - Volume 8483

June 2014

342 pages

ISBN:9783319073163

Editors:
Marco Bernardo
Dipartimento di Scienze di Base e Fondamenti, Universití di Urbino, Urbino, Italy
,
Ferruccio Damiani
Dipartimento di Informatica, Universití di Torino, Torino, Italy
,
Reiner Hähnle
Fachbereich Informatik, Technische Universität Darmstadt, Darmstadt, Germany
,
Einar Johnsen
Department of Informatics, University of Oslo, Oslo, Norway
,
Ina Schaefer
Institut für Softwaretechnik und Fahrzeuginformatik, Technische Universität Braunschweig, Braunschweig, Germany

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 16 June 2014

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Aminof BKotek TRubin SSpegni FVeith H(2018)Parameterized model checking of rendezvous systemsDistributed Computing10.1007/s00446-017-0302-631:3(187-222)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s00446-017-0302-6
Konnov ILazić MVeith HWidder J(2017)A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsACM SIGPLAN Notices10.1145/3093333.300986052:1(719-734)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009860
Konnov ILazić MVeith HWidder JCastagna GGordon A(2017)A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009860(719-734)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009860
Konnov ILazić MVeith HWidder J(2017)Para$$^2$$2Formal Methods in System Design10.1007/s10703-017-0297-451:2(270-307)Online publication date: 1-Nov-2017
https://dl.acm.org/doi/10.1007/s10703-017-0297-4
Delzanno G(2016)A unified view of parameterized verification of abstract models of broadcast communicationInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-016-0412-718:5(475-493)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1007/s10009-016-0412-7
Bérard BLafourcade PMillet LPotop-Butucaru MThierry-Mieg YTixeuil S(2016)Formal verification of mobile robot protocolsDistributed Computing10.1007/s00446-016-0271-129:6(459-487)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1007/s00446-016-0271-1

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents