More Web Proxy on the site http://driver.im/

research-article

Open access

Formalizing process algebraic verifications in the calculus of constructions

Authors:

Jan Friso GrooteAuthors Info & Claims

Formal Aspects of Computing, Volume 9, Issue 1

Pages 1 - 48

https://doi.org/10.1007/BF01212523

Published: 01 January 1997 Publication History

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.

References

References

[1]

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.

[2]

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.

[3]

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.

[4]

Bezem M. and Groote J. F. A correctness proof of a one-bit sliding window protocol inμCRL The Computer Journal 1994 37 4 289-307

[5]

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.

[6]

Bezem, M. and Groote, J. F.: Proving a graph well founded using resolution. Technical Report 113, Logic Group Preprint Series, Utrecht University, May 1994.

[7]

Bergstra J. A. and Klop J. W. Hazewinkel M., Lenstra J. K., and Meertens L. G. L. T. Process algebra: specification and verification in bisimulation semantics Mathematics and Computer Science II 1986 Amsterdam North-Holland 61-94

[8]

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.

[9]

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 1969 12 260-261

Digital Library

[10]

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

[11]

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 1986 first edition Englewood Cliffs, New Jersey Prentice-Hall, inc.

[12]

Coquand T. and Huet G. The calculus of constructions Information and Control 1988 76 95-120

Digital Library

[13]

Courcoubetis C Proceedings of the 5th International Conference on Computer Aided Verification 1993 editor Elounda, Greece Springer-Verlag

Digital Library

[14]

Cleaveland R. and Panangaden P. Type theory and concurrency International Journal of Parallel Programming 1988 17 153-206

Digital Library

[15]

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.

[16]

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.

[17]

Drost, N. J.:Process Theory and Equation Solving. PhD thesis, University of Amsterdam, February 1994. (Section 2.5.1).

[18]

Engberg U., Grønning P., and Lamport L. Bochmann G. v. and Probst D. K. Mechanical verification of concurrent systems with TLA volume 663 ofLecture Notes in Computer Science 1992 Montreal, Canada Springer-Verlag 44-55

[19]

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.

[20]

Groote J. F. and Ponse A. Andrews D. J., Groote J. F., and Middelburg C. A. Proof theory for μCRL: a language for processes with data Proceedings of the International Workshop on Semantics of Specification Languages 1993 Utrecht, The Netherlands Workshops in Computer Science, Springer-Verlag 231-250

[21]

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.

[22]

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.

[23]

Groote, J. F. and van Wamel, J. J.: Algebraic data types and induction in μCRL. Technical Report P9409, University of Amsterdam, April 1994.

[24]

Hesselink W. H. Wait-free linearization with an assertional proof Distributed Computing 1994 8 65-80

Digital Library

[25]

Hesselink, W. H.: Wait-free linearization with a mechanical proof.Distributed Computing, 9:(to appear), 1995.

[26]

Hooman, J.:Specification and Compositional Verification of Real-Time Systems, LNCS 558. PhD thesis, Eindhoven University of Technology, 1991.

[27]

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.

[28]

Kamsteeg G. A formal verification of the Alternating Bit Protocol in μCRL. Technical Report 1993 Netherlands Dept. of Comp. Sci., Leiden University 93-37

[29]

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.

[30]

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).

[31]

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.

[32]

Lynch, N., Merritt, M., Weihl, W. and Fekete, A.:Atomic Transactions. Morgan Kaufmann Publishers, 1994.

[33]

Milner, R.:A Calculus of Communicating Systems, volume 92 ofLecture Notes in Computer Science. Springer-Verlag, 1980.

[34]

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.

[35]

Owicki S. and Lamport L. Proving liveness properties of concurrent programs ACM Transactions on Programming Languages and Systems 1982 4 3 455-495

Digital Library

[36]

Paulin-Mohring, G: Inductive definitions in the system Coq. InTyped Lambda Calculi and Applications, LNCS 664, pages 328–345, 1993.

[37]

van de Pol, J. and Sellink, M. P. A.: Personal communication, 1993.

[38]

Sellink M. P. A. Andrews D. J., Groote J. F., and Middelburg C. A. Verifying process algebra proofs in type theory Proceedings of the International Work-shop on Semantics of Specification Languages 1993 Utrecht, The Netherlands Workshops in Computer Science, Springer-Verlag 315-339

[39]

Sellink, M. P. A.: On the conservativity of Liebniz equality. Technical Report P9611, Programming Research Group, University of Amsterdam, 1996.

[40]

Werner, B.:Une théorie des Constructions Inductives. PhD thesis, Université de Paris 7, May 1994.

Cited By

Balabonski TCourtieu PPelle RRieg LTixeuil SUrbain X(2021)Computer Aided Formal Design of Swarm Robotics AlgorithmsStabilization, Safety, and Security of Distributed Systems10.1007/978-3-030-91081-5_31(469-473)Online publication date: 17-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-91081-5_31
Potop-Butucaru MSznajder NTixeuil SUrbain X(2019)Formal Methods for Mobile RobotsDistributed Computing by Mobile Entities10.1007/978-3-030-11072-7_12(278-313)Online publication date: 13-Jan-2019
https://doi.org/10.1007/978-3-030-11072-7_12
Dubois CGrinchtein OPearson JCarlsson M(2018)Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem ProverSoftware Engineering and Formal Methods10.1007/978-3-319-92970-5_15(239-253)Online publication date: 30-May-2018
https://doi.org/10.1007/978-3-319-92970-5_15
Show More Cited By

Index Terms

Formalizing process algebraic verifications in the calculus of constructions

Index terms have been assigned to the content through auto-classification.

Recommendations

Formalizing Type Operations Using the “Image” Type Constructor

In this paper we introduce a new approach to formalizing certain type operations in type theory. Traditionally, many type constructors in type theory are independently axiomatized and the correctness of these axioms is argued semantically. In this paper ...
Soundness of Coercion in the Calculus of Constructions

A coercive subtyping system for the Calculus of Constructions is presented. The proposed system λC_≤^co is obtained essentially by adding coercions and η-conversion to λC_≤, which is a subtyping extension to the Calculus of Constructions without coercions. ...
Coercive subtyping for the calculus of constructions

We present a coercive subtyping system for the calculus of constructions. The proposed system λC^COover≤ is obtained essentially by adding coercions and η-conversion to λC_≤[10], which is a subtyping extension to the calculus of constructions without ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 9, Issue 1

Jan 1997

118 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© BCS 1997.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 January 1997

Accepted: 15 November 1995

Received: 15 December 1994

Published in FAC Volume 9, Issue 1

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
59
Total Downloads

Downloads (Last 12 months)39
Downloads (Last 6 weeks)5

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Balabonski TCourtieu PPelle RRieg LTixeuil SUrbain X(2021)Computer Aided Formal Design of Swarm Robotics AlgorithmsStabilization, Safety, and Security of Distributed Systems10.1007/978-3-030-91081-5_31(469-473)Online publication date: 17-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-91081-5_31
Potop-Butucaru MSznajder NTixeuil SUrbain X(2019)Formal Methods for Mobile RobotsDistributed Computing by Mobile Entities10.1007/978-3-030-11072-7_12(278-313)Online publication date: 13-Jan-2019
https://doi.org/10.1007/978-3-030-11072-7_12
Dubois CGrinchtein OPearson JCarlsson M(2018)Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem ProverSoftware Engineering and Formal Methods10.1007/978-3-319-92970-5_15(239-253)Online publication date: 30-May-2018
https://doi.org/10.1007/978-3-319-92970-5_15
Auger CBouzid ZCourtieu PTixeuil SUrbain X(2013)Certified Impossibility Results for Byzantine-Tolerant Mobile RobotsStabilization, Safety, and Security of Distributed Systems10.1007/978-3-319-03089-0_13(178-190)Online publication date: 2013
https://doi.org/10.1007/978-3-319-03089-0_13
Stappers FReniers MWeber SGroote J(2012)Dogfooding the Formal Semantics of mCRL2Proceedings of the 2012 35th Annual IEEE Software Engineering Workshop10.1109/SEW.2012.16(90-99)Online publication date: 12-Oct-2012
https://dl.acm.org/doi/10.1109/SEW.2012.16
Stappers FReniers MWeber S(2011)Transforming SOS Specifications to Linear ProcessesFormal Methods for Industrial Critical Systems10.1007/978-3-642-24431-5_15(196-211)Online publication date: 2011
https://doi.org/10.1007/978-3-642-24431-5_15
Groote JMonin Fvan de Pol J(2006)Checking verifications of protocols and distributed systems by computerCONCUR'98 Concurrency Theory10.1007/BFb0055652(629-655)Online publication date: 28-May-2006
https://doi.org/10.1007/BFb0055652
Groote JReniers M(2001)Algebraic Process VerificationHandbook of Process Algebra10.1016/B978-044482830-9/50035-7(1151-1208)Online publication date: 2001
https://doi.org/10.1016/B978-044482830-9/50035-7
Basten THooman J(1999)Process Algebra in PVSTools and Algorithms for the Construction and Analysis of Systems10.1007/3-540-49059-0_19(270-284)Online publication date: 12-Mar-1999
https://doi.org/10.1007/3-540-49059-0_19

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Figures

Tables

Media

View Issue’s Table of Contents