Abstract
This paper reports on the first steps towards the formal verification of correctness proofs of real-life protocols in process algebra. We show that such proofs can be verified, and partly constructed, by a general purpose proof checker. The process algebra we use isμCRL, ACPτ augmented with data, which is expressive enough for the specification of real-life protocols. The proof checker we use is Coq, which is based on the Calculus of Constructions, an extension of simply typed lambda calculus. The focus is on the translation of the proof theory ofμCRL andμCRL-specifications to Coq. As a case study, we verified the Alternating Bit Protocol.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Barendregt, H. P.: Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors,Handbook of Logic in Computer Science, pages 117–309. Oxford University Press, 1992.
Baeten, J. C. M. and Bergstra, J. A.: Discrete time process algebra. In W. R. Cleaveland, editor,Proceedings Concur'92, LNCS 630, pages 401–20. Springer Verlag, 1992.
Bezem, M. and Groote, J. F.: A formal verification of the alternation bit protocol in the calculus of constructions. Technical Report 88, Logic Group Preprint Series, Utrecht University, March 1993.
Bezem, M. and Groote, J. F.: A correctness proof of a one-bit sliding window protocol inμCRL.The Computer Journal, 37(4):289–307, 1994.
Bezem, M. and Groote, J. F.: Invariants in process algebra with data. In B. Jonsson and J. Parrow, editors,Proceedings Concur'94, LNCS 836, pages 401–416. Springer Verlag, 1994.
Bezem, M. and Groote, J. F.: Proving a graph well founded using resolution. Technical Report 113, Logic Group Preprint Series, Utrecht University, May 1994.
Bergstra, J. A. and Klop, J. W.: Process algebra: specification and verification in bisimulation semantics. In M. Hazewinkel, J. K. Lenstra, and L. G. L. T. Meertens, editors,Mathematics and Computer Science II, CWI Monograph 4, pages 61–94. North-Holland, Amsterdam, 1986.
Bergstra, J. A. and Klop, J. W.: Verification of an alternating bit protocol by means of process algebra. In W. Bibel and K. P Jantke, editors,Math. Methods of Spec, and Synthesis of Software Systems 1985, LNCS 215, pages 9–23. Springer Verlag, 1986.
Bartlett, K. A., Scantlebury, R. A. and Wilkinson, P. T.: A note on reliable full-duplex transmission over half-duplex links.Communications of the ACM, 12:260–261, 1969.
Baeten, J. C. M. and Weijland, W. P.:Process Algebra, volume 18 ofCambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.
Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendier, N. P., Panangaden, P., Sasaki, J. T. and Smith, S. F.:Implementing Mathematics with the NuPrl Development System. Prentice-Hall, inc., Englewood Cliffs, New Jersey, first edition, 1986.
Coquand, T. and Huet, G.: The calculus of constructions.Information and Control, 76:95–120, 1988.
Courcoubetis, C: editor.Proceedings of the 5th International Conference on Computer Aided Verification, Elounda, Greece, June/July 1993. Springer-Verlag, 1993.
Cleaveland, R. and Panangaden, P.: Type theory and concurrency.International Journal of Parallel Programming, 17:153–206, 1988.
Coquand, T. and Paulin, G: Inductively Defined Types. In P. Martin-Löf and G. Mints, editors,COLOG-88, LNCS 417, pages 50–66. Springer-Verlag, 1990.
Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, G, Parent, C, Paulin-Mohring, C. and Werner, B.: The Coq Proof Assistant User's Guide, version 5.8. Technical report, INRIA-Rocquencourt and CNRS - ENS Lyon, 1993.
Drost, N. J.:Process Theory and Equation Solving. PhD thesis, University of Amsterdam, February 1994. (Section 2.5.1).
Engberg, U., Grønning, P. and Lamport, L.: Mechanical verification of concurrent systems with TLA. In G. v. Bochmann and D. K. Probst, editors,Proceedings of the 4th International Workshop on Computer Aided Verification, Montreal, Canada, volume 663 ofLecture Notes in Computer Science, pages 44–55. Springer-Verlag, 1992.
Giménez, E.: Co-Inductive Types in Coq: An Experiment with the Alternating Bit Protocol. Submitted for the proceedings of the BRA Workshop on Types for Proofs and Programs. Also available by ftp at ftp.ens-lyon.fr/pub/users/LIP/ABP.ps.Z, June 1995.
Groote, J. F. and Ponse, A.: Proof theory for μCRL: a language for processes with data. In D. J. Andrews, J. F. Groote, and C. A. Middelburg, editors,Proceedings of the International Workshop on Semantics of Specification Languages, Utrecht, The Netherlands, pages 231–250. Workshops in Computer Science, Springer-Verlag, 1993.
Groote, J. F. and Ponse, A.: The syntax and semantics of μCRL. In A. Ponse, C. Verhoef, and S. F. M van Vlijmen, editors, Algebra of Communicating Processes (Proceedings ACP'94), pages 26–62, 1994.
Groote, J. F. and van de Pol, J. C.: A bounded retransmission protocol for large data packets. A case study in computer checked verification. In M. Wissing and M. Nivat, editors,Proceedings of AMAST'96, Munich, Lecture Notes in Computer Science 1101, Springer Verlag, pages 536–550, 1996.
Groote, J. F. and van Wamel, J. J.: Algebraic data types and induction in μCRL. Technical Report P9409, University of Amsterdam, April 1994.
Hesselink, W. H.: Wait-free linearization with an assertional proof.Distributed Computing, 8:65–80, 1994.
Hesselink, W. H.: Wait-free linearization with a mechanical proof.Distributed Computing, 9:(to appear), 1995.
Hooman, J.:Specification and Compositional Verification of Real-Time Systems, LNCS 558. PhD thesis, Eindhoven University of Technology, 1991.
Helmink, L., Sellink, M. P. A. and Vaandrager, F. W.: Proof-checking a data link protocol. InProceedings Workshop Esprit BRA Types for Proofs and Programs, Nijmegen, The Netherlands, May 1993, LNCS 806. Springer-Verlag, 1994.
Kamsteeg, G.: A formal verification of the Alternating Bit Protocol in μCRL. Technical Report 93–37, Dept. of Comp. Sci., Leiden University, Netherlands, 1993.
Klusener, A. S.: Abstraction in real time process algebra. In J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg, editors,Proceedings of the REX workshop “Real-Time: Theory in Practice”, LNCS 600. Springer-Verlag, 1991.
Kaart, M. and Polak, I.: Het alternating bit protocol met time-out in discrete tijd. Technical Report P9323, Programming Research Group, University of Amsterdam, September 1993. (in Dutch).
Korver, H. and Springintveld, J.: A computer-checked verification of Milner's Scheduler. In: M. Hagiya, J. C. Mitchell, editors,Proceedings TACS'94, Sendai Japan, Lecture Notes in Computer Science 789, pages 161–178. Springer-Verlag 1994. Full version: Technical Report 101, Logic Group Preprint Series, Utrecht University, November 1993.
Lynch, N., Merritt, M., Weihl, W. and Fekete, A.:Atomic Transactions. Morgan Kaufmann Publishers, 1994.
Milner, R.:A Calculus of Communicating Systems, volume 92 ofLecture Notes in Computer Science. Springer-Verlag, 1980.
Manna, Z. and Pnueli, A.: Verification of concurrent programs, a temporal proof system. InFoundations of Computer Science IV, Distributed Systems: Part 2 Mathematical Centre Tracts 159, pages 163–255, 1982.
Owicki, S. and Lamport, L.: Proving liveness properties of concurrent programs.ACM Transactions on Programming Languages and Systems, 4(3):455–495, 1982.
Paulin-Mohring, G: Inductive definitions in the system Coq. InTyped Lambda Calculi and Applications, LNCS 664, pages 328–345, 1993.
van de Pol, J. and Sellink, M. P. A.: Personal communication, 1993.
Sellink, M. P. A.: Verifying process algebra proofs in type theory. In D. J. Andrews, J. F. Groote, and C. A. Middelburg, editors,Proceedings of the International Work-shop on Semantics of Specification Languages, Utrecht, The Netherlands, pages 315–339. Workshops in Computer Science, Springer-Verlag, 1993.
Sellink, M. P. A.: On the conservativity of Liebniz equality. Technical Report P9611, Programming Research Group, University of Amsterdam, 1996.
Werner, B.:Une théorie des Constructions Inductives. PhD thesis, Université de Paris 7, May 1994.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Bezem, M., Bol, R. & Groote, J.F. Formalizing process algebraic verifications in the calculus of constructions. Formal Aspects of Computing 9, 1–48 (1997). https://doi.org/10.1007/BF01212523
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF01212523