Skip to main content
SpringerLink
Log in

Checking verifications of protocols and distributed systems by computer

  • Conference paper
  • First Online:
CONCUR'98 Concurrency Theory (CONCUR 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1466))

Included in the following conference series:

Abstract

We provide a treatise about checking proofs of distributed systems by computer using general purpose proof checkers. In particular, we present two approaches to verifying and checking the verification of the Sequential Line Interface Protocol (SLIP), one using rewriting techniques and one using the so-called cones and foci theorem. Finally, we present an overview of literature containing checked proofs.

The research of the second author is supported by Human Capital Mobility (HCM).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G.J. Akkerman and J.C.M. Baeten. Term rewriting analysis in process algebra. Technical report CS-R9130. CWI, Amsterdam, 1991.

    Google Scholar 

  2. M. Archer and C. Heitmeyer. Mechanical verification of timed automata: A case study. In Proceedings 1996 IEEE Real-Time Technology and Applications Symposium (RTAS'96). IEEE Computer Society Piess, 1996.

    Google Scholar 

  3. M. Archer and C. Heitmeyer. Verifying hybrid systems modeled as timed automata: a case study. In O. Maler, editor, International Workshop, Hybrid and Real-Time Systems, HART'97, volume 1201 of Lecture Notes in Computer Science, pages 171–185, Springer-Verlag, 1997.

    Google Scholar 

  4. M.M. Ayadi and D.D. Bolignagno. On the formal verification of delegation in SESAME. IEEE COMPASS, pages 23–34, 1997.

    Google Scholar 

  5. J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 1990.

    Google Scholar 

  6. G. Bella and L.C. Paulson. Using Isabelle to prove properties of the Kerberos authentication system. In H. Orman and C. Meadows, editors, Workshop on Design and Formal Verification of Security Protocols. DIMACS, 1997.

    Google Scholar 

  7. M.A. Bezem, R. Bol and J.F. Groote. Formalizing process algebraic verifications in the calculus of constructions. Formal Aspects of Computing, 9(1):1–48, 1997.

    Article  MATH  Google Scholar 

  8. M.A. Bezem and J.F. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Technical Report 88, Logic Group Preprint Series, Utrecht University, March 1993.

    Google Scholar 

  9. M.A. Bezem and J.F. Groote. Invariants in process algebra with data. In B. Jonsson and J. Parrow, editors, Proceedings Concur'94, Uppsala, Sweden, Lecture Notes in Computer Science no. 836, pages 401–416, Springer Verlag, 1994.

    Google Scholar 

  10. D. Bosscher and A. Ponse. Translating a process algebra with symbolic data values to linear format. In U.H. Engberg, K.G. Larsen, and A. Skou, editors, Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Aarhus 1995, BRICS Notes Series, pages 119–130. University of Aarhus, 1995.

    Google Scholar 

  11. R. Bharadwaj, A. Felty and F. Stomp. Formalizing inductive proofs of network algorithms. In Proceedings of the 1995 Asian Computing Science Conference, 1995.

    Google Scholar 

  12. R.S.. Boyer, J.S. Moore: A Computational Logic Handbook. Academic Press, Boston etc., 1988.

    Google Scholar 

  13. D. Bolignagno and V. Menissier-Morain. Formal verification of cryptographic protocols using Coq. Technical Report, INRIA-Rocquencourt, 1996.

    Google Scholar 

  14. D.J.B. Bosscher, I. Polak and F.W. Vaandrager. Verification of an audio control protocol. In H. Langmaack, W.P. de Roever and J. Vytopil, editors, Proceedings of the third School and Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 170–192, Springer-Verlag, 1994.

    Google Scholar 

  15. R. Cardell-Oliver. The specification and verification of a sliding window protocol. Computer Laboratory Technical Report 183, University of Cambridge, 1989.

    Google Scholar 

  16. K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, Massachusetts, 1988. ISBN 0-201-05866-9.

    Google Scholar 

  17. B. Chetali. Formal verification of concurrent programs using the larch prover. In U.H. Engberg, K.G. Larsen and A. Skou, editors, Proceedings of the Workshop on Tools and Algorithms for the Constructions and Analysis of Systems, BRICS Notes, pages 174–186, Aarhus, Denmark, May 1995.

    Google Scholar 

  18. B. Chetali and P. Lescanne. Formal verification of a protocol for communications over faulty channels. In G. v. Bochmann, R. Dssouli and O. Rafiq, editors, Proceedings of the IFIP TC6 Eighth International Conference on Formal Description Techniques, pages 91–108, 1995.

    Google Scholar 

  19. P. Crégut and B. Heyd. COQ-Unity. In Actes des journées du GDR Programmation.

    Google Scholar 

  20. M.C.A. Devillers, W.O.D. Griffioen, J.M.T. Romijn and F.W. Vaandrager. Verification of a leader election protocol: formal methods applied to IEEE 1394. Report CSI-R9728, Computing Science Institute, Nijmegen, 1997.

    Google Scholar 

  21. D. Dolev and N. Shavit. Bounded concurrent time-stamping. SIAM Journal on Computing 26(2):418–455, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  22. G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq Proof Assistant User's Guide, version 5.8, INRIA-Rocquencourt and CNRS — ENS Lyon 1993.

    Google Scholar 

  23. U. Engberg. Reasoning in the temporal logic of actions. The design and implementation of an interactive computer system. PhD thesis, Department of Computer Science, University of Aarhus, September 1995.

    Google Scholar 

  24. U. Engberg, P. GrØnning and L. Lamport. Mechanical verification of concurrent systems with TLA. In G. v. Bochmann and D.K. Probst, editors, Proceedings of the Fourth International Conference on Computer Aided Verification (CAV'92), LNCS 663, pages 44–55, Springer-Verlag, 1992.

    Google Scholar 

  25. R.G. Gallager, P.A. Humblet, P.M. Spira: A distributed algorithm for minimal-weight spanning trees. ACM Transactions on Programming languages 5(1):66–77, 1983.

    Article  MATH  Google Scholar 

  26. R. Gawlick, N.A. Lynch and N. Shavit. Concurrent timestamping made simple. Israel Symposium on Theory and Practice of Computing, 1992.

    Google Scholar 

  27. E. Gimenez. An application of co-inductive types in Coq: verification of the alternating bit protocol. In Proceedings of the Workshop on Types for Proofs and Programs, volume 1158 of Lecture Notes in Computer Science, pages 135–152, Springer-Verlag, 1996.

    Google Scholar 

  28. D.M. Goldschlag. Mechanically verifying concurrent programs with the Boyer-Moore prover. IEEE Transactions on Software Engineering SE-16(9): 1005–1022, September 1990.

    Article  Google Scholar 

  29. D.M. Goldschlag. Verifying safety and liveness properties of a delay insensitive fifo circuit on the Boyer-Moore prover. International Workshop on Formal Methods in VSLI Design, 1991.

    Google Scholar 

  30. D. Gaigen, S. Kromodimoeljo, I. Meisels, W. Pase and M. Saaltink. EVES: An overview. In S. Prehn and H. Toetenel editors, Proceedings of Formal Software Development Methods, VDM'91, volume 552 of Lecture Notes in Computer Science, pages 389–405, Springer-Verlag, 1991.

    Google Scholar 

  31. M.J.C. Gordon and T.F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge, 1993.

    Google Scholar 

  32. W.O.D. Griffioen. Proof-checking an audio control protocol with LP. Report CS-R9570, CWI, Amsterdam, 1995.

    Google Scholar 

  33. J.F. Groote, F. Monin and J. Springintveld. A computer checked algebraic verification of a distributed summing protocol. Computer Science Report 97-14, Department of Mathematics and Computer Science, Eindhoven, 1997.

    Google Scholar 

  34. J.F. Groote and A. Ponse. The syntax and semantics of ΜCRL. In A. Ponse, C. Verhoef and S.F.M. van Vlijmen, eds, Algebra of Communicating Processes, Workshops in Computing, pp. 26–62, 1994.

    Google Scholar 

  35. J.F. Groote and J. Springintveld. Focus points and convergent process operators. A proof strategy for protocol verification. Technical Report 142, Logic Group Preprint Series, Utrecht University, 1995. This report also appeared as Technical Report CS-R9566, Centrum voor Wiskunde en Informatica, 1995

    Google Scholar 

  36. J.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large data packets. A case study in computer checked verification. In M. Wirsing and M. Nivat, editors, Proceedings of AMAST'96, volume 1101 of Lecture Notes in Computer Science, pages 536–550, Springer-Verlag, 1996.

    Google Scholar 

  37. J.V. Guttag, J.J. Horning (eds.) with S.J. Garland, K.D. Jones, A. Modet and J.M. Wing. Larch: languages and tools for formal specifications. Texts and Monographs in Computer Science, Springer, 1993.

    Google Scholar 

  38. K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In M.C. Gaudel and J. Woodcock, editors, Third International Symposium of Formal Methods Europe (FME'96), volume 1051 of Lecture Notes in Computer Science, pages 662–681, 1996.

    Google Scholar 

  39. L. Helmink, M.P.A. Sellink and F.W. Vaandrager. Proof-checking a data link protocol. In H. Barendregt and T. Nipkow, editors, Proceedings International Workshop TYPES'93, volume 806 of Lecture Notes in Computer Science, pages 127–165, Springer-Verlag, 1994.

    Google Scholar 

  40. C. Heitmeyer and A.N. Lynch. The Generalized Railroad Crossing: A case study in formal verification of real-time systems. In Proceedings of the 15th IEEE Real-Time Systems Symposium, pages 120–131, 1994.

    Google Scholar 

  41. W.H. Hesselink. The verified incremental design of a distributed spanning tree algorithm. Computing Science Reports CS-R9602, Groningen 1996.

    Google Scholar 

  42. W.H. Hesselink. A mechanical proof of Segall's PIF algorithm. Formal Aspects of Computing, 9(2):208–226, 1997.

    Article  MATH  Google Scholar 

  43. J. Hooman. Verifying part of the ACCESS bus protocol using PVS. In P.S. Thiagarajan, editor, 15th Conference on the Foundations of Software Technology and Theoretical Computer Science, LNCS 1026, pages 96–110, Springer-Verlag, 1995.

    Google Scholar 

  44. J. Hooman. Verification of distributed real-time and fault-tolerant protocols. In M. Johnson, editor, Sixth International Conference on Algebraic Methodology and Software Technology, AMSAT'97, volume 1349 of Lecture Notes in Computer Science, pages 261–275, Springer-Verlag, 1997.

    Google Scholar 

  45. J. Hooman. Formal verification of the binary exponential backoff protocol. In M. Johnson, editor, Proceedings ninth Nordic Workshop on Programming Theory, 1998.

    Google Scholar 

  46. M. Kaufmann and J.S. Moore. ACL2: Industrial strength version of Nqthm. Transactions on Software Engineering, 1997.

    Google Scholar 

  47. H.P. Korver and J. Springintveld. A computer-checked verification of Milner's scheduler. In M. Hagiya and J.C. Mitchell, editors, Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS'94), LNCS 789, pages 161–178, Springer-Verlag, 1994.

    Google Scholar 

  48. H. Korver and A. Sellink. On automating process algebra proofs. Technical Report 154, Logic Group Preprint Series, Utrecht University, 1996.

    Google Scholar 

  49. R.P. Kurshan and L. Lamport. Verification of multiplier: 64 bits and beyond. In C. Courcoubetis, editor, Proceedings of the Fifth International Conference on Computer Aided Verification (CAV'93), volume 697 of Lecture Notes in Computer Science, pages 166–179, Springer-Verlag, 1993.

    Google Scholar 

  50. L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, 1994.

    Article  Google Scholar 

  51. G. Leeb and N.A. Lynch. Proving safety properties of the Steam Boiler Controller: Formal methods for industrial applications: A case study. In J.-R. Abrial, et al., editors, Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control LNCS 1165, Springer-Verlag, 1996.

    Google Scholar 

  52. D. Lesens and H. Saidi. Automatic verification of parameterized networks of processes by abstraction. In Proceedings of the Second International Workshop on the Verification of Infinite State Systems (INFINITY'97), 1997.

    Google Scholar 

  53. P. Lincoln and J. Rushby. The formal verification of an algorithm for interactive consistency under a hybrid fault model. In C. Courcoubetis, editor, Fifth International Conference on Computer-Aided Verification (CAV'93), volume 697 of Lecture Notes in Computer Science, pages 305–319, Springer-Verlag, 1993.

    Google Scholar 

  54. P. Loewenstein and D.L. Dill. Verification of a multiprocessor cache protocol using simulation relations and higher-order logic. In E.M. Clarke and R.P. Kurshan, editors, Second International Conference Computer-Aided Verification (CAV'90), LNCS 531, Springer-Verlag, pages 303–311, 1990.

    Google Scholar 

  55. V. Lunchangco, E. Söylemez, S.J. Garland and N.A. Lynch. Verifying timing properties of concurrent algorithms. In D. Hogrefe and S. Leue, editors, Proceedings of the Seventh International Conference on Formal Description Techniques for Distributed Systems (FORTE'94), pages 259–273, IFIP WG6.1, Chapman&Hall, 1995.

    Google Scholar 

  56. N.A. Lynch and F.W. Vaandrager. Forward and backward simulations for timing-based systems. In J.W. de Bakker, C. Huizing and G. Rozenberg, editors. Proceedings of REX Workshop ”Real-Time: Theory in Practice”, volume 600 of Lecture Notes in Computer Science, pages 397–446. Springer-Verlag, 1992.

    Google Scholar 

  57. N.A. Lynch and M. Tuttle. An introduction to Input/Output automata. CWI Quarterly 2(3):219–246, 1989.

    MATH  MathSciNet  Google Scholar 

  58. Z. Manna and A. Pnueli. Verification of concurrent programs: the temporal framework. In R.S. Boyer and J.S. Moore, editors, The correctness Problem in Computer Science, Academic Press, London, 1981.

    Google Scholar 

  59. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

    Google Scholar 

  60. A. Mokkedem, M.J. Ferguson and R.B. Johnston. A TLA solution to the specification and verification of the RLP1 retransmission protocol. In J. Fitzgerald, C.B. Jones and P. Lucas, editors, Proceedings of the Fourth International Symposium of Formal Methods Europe (FME'97), volume 1313 of Lecture Notes in Computer Science. Springer-Verlag, 1997.

    Google Scholar 

  61. J.S. Moore. A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol. Journal of Formal Aspects of Computing Science 6(1):60–91, 1994.

    Article  MATH  Google Scholar 

  62. O. Müller and T. Nipkow. Traces of I/O automata in Isabelle/HOLCF. In M. Bidoit and M. Dauchet, editors, Proceedings of the Seventh International Joint on the Theory and Practice of Software Development (TAPSOFT'97), LNCS 1214, pages 580–595, Springer-Verlag, 1997.

    Google Scholar 

  63. M. Nagayama and C. Talcott. An NQTHM mechanization of an exercise in the verification of multi-process programs. Technical Report STAN-CS-91-1370, Stanford University, 1991.

    Google Scholar 

  64. T. Nipkow and K. Slind. I/O automata in Isabelle/HOL. In P. Dybjer, B. Nordström and J.Smith, editors, Proceedings of the International Workshop on Types for Proofs and Programs, volume 996 of Lecture Notes in Computer Science, pages 101–119, Springer-Verlag, 1994.

    Google Scholar 

  65. L.C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–386. Academic Press, 1990.

    Google Scholar 

  66. L.C. Paulson. Isabelle: A Generic Theorem Prover. Springer-Verlag LNCS 828, 1994.

    Google Scholar 

  67. L.C. Paulson. On two formal analyses of the Yahalom protocol. Technical Report 432, Computer Laboratory, University of Cambridge, 1997.

    Google Scholar 

  68. L.C. Paulson. Inductive analysis of the internet protocol TLS. Technical Report 440, Computer Laboratory, University of Cambridge, 1997.

    Google Scholar 

  69. L.C. Paulson. The inductive approach to verifying cryptographic protocols. Computer Security Journal, to appear 1998.

    Google Scholar 

  70. T.P. Petrov, A. Pogosyants, S.J. Garland, V. Lunchangco and N.A. Lynch. Computer-assisted verification of an algorithm for concurrent timestamps. In R. Gotzhein and J. Bredereke, editors, Formal Description Techniques IX: Theory, Applications, and Tools, (FORTE/PTSV'96: Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification), pages 29–44, Chapman&Hall, 1996.

    Google Scholar 

  71. J. Rushby and F. von Henke. Formal verification of a fault-tolerant clock synchronization algorithm. NASA Contractor Report 4239, 1989.

    Google Scholar 

  72. D.M. Russinoff. Verifying concurrent programs with the Boyer-Moore Prover. Technical Report STP/ACT-218-90, MCC, Austin, Texas, 1990.

    Google Scholar 

  73. D.M. Russinoff. A Mechanically verified incremental garbage collector. Technical Report STP/ACT-91, MCC, Austin, Texas, 1991.

    Google Scholar 

  74. N. Shankar. Mechanical verification of a generalized protocol for Byzantine faulttolerant clock synchronization. In J. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of Lecture Notes in Computer Science, pages 217–236, 1992.

    Google Scholar 

  75. N. Shankar. Verification of real-time systems using PVS. In C. Courcoubetis, editor, Fifth Conference on Computer-Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 280–291, Springer-Verlag, 1993.

    Google Scholar 

  76. N. Shankar, S. Owre and J.M. Rushby. The PVS Proof Checker: A Reference Manual. Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993.

    Google Scholar 

  77. J.F. SØgaard-Andersen, S.J. Garland, J.V. Guttag, N.A. Lynch and A. Pogosyants. Computer-assisted simulation proofs. In C, Courcoubetis, editor, Fifth International on Computer-Aided Verification (CAV'93), volume 697 of Lecture Notes in Computer Science, pages 305–319, Springer-Verlag, 1993.

    Google Scholar 

  78. J. Vitt and J. Hooman. Assertional specification and verification using PVS of the Steam Boiler Control system. In J.-R. Abrial, et al., editors, Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control volume 1165 of Lecture Notes in Computer Science, 1996.

    Google Scholar 

  79. J. von Wright and T. Långbacka. Using a theorem prover for reasoning about concurrent algorithms. In G. v. Bochmann and D.K. Probst, editors, Proceedings of the Fourth International Conference on Computer Aided Verification(CAV'92), volume 663 of Lecture Notes in Computer Science, pages 56–68, Springer-Verlag, 1992.

    Google Scholar 

  80. W.D. Young. Verifying the interactive convergence clock synchronization algorithm using the Boyer-Moore theorem prover. Contractor Report 189649, NASA, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, P.O. Box 94079, 1090, GB Amsterdam, The Netherlands

    Jan Friso Groote

  2. Department of Mathematics and Computing Science, Eindhoven University of Technology, P.O. Box 513, 5600, MB Eindhoven, The Netherlands

    Jan Friso Groote, FranÇois Monin & Jaco van de Pol

Authors
  1. Jan Friso Groote
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. FranÇois Monin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jaco van de Pol
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Davide Sangiorgi Robert de Simone

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Groote, J.F., Monin, F., van de Pol, J. (1998). Checking verifications of protocols and distributed systems by computer. In: Sangiorgi, D., de Simone, R. (eds) CONCUR'98 Concurrency Theory. CONCUR 1998. Lecture Notes in Computer Science, vol 1466. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055652

Download citation

  • DOI: https://doi.org/10.1007/BFb0055652

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64896-3

  • Online ISBN: 978-3-540-68455-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation