Advertisement

Proof Theory for µCRL: A Language for Processes with Data.

  • Jan Friso Groote
  • Alban Ponse
Part of the Workshops in Computing book series (WORKSHOPS COMP.)

Abstract

A simple specification language, called µCRL (micro Common Representation Language), is introduced. It consists of process algebra extended with abstract data types. The language µCRL is designed such that it contains only basic constructs with a straightforward semantics. It has been developed under the assumption that an extensive and mathematically precise study of these constructs and their interaction will yield fundamental insights that are are essential to an analytical approach of well-known and much richer specification languages. To this end, a simple property language is defined in which basic properties of processes, data and the process/data relationship can be expressed in a formal way. Next a proof system is defined for this property language, comprising a rule for induction, the Recursive Specification Principle, and process algebra axioms. The proof theory thus obtained is designed such that automatic proof checking is feasible. It is illustrated with a case study of a counter.

Keywords

Proof System Process Counter Data Term Proof Theory Process Algebra 
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]
    J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.Google Scholar
  2. [2]
    J.A. Bergstra, I. Bethke, and A. Ponse. Process algebra with combinators. Report P9319, Programming Research Group, University of Amsterdam, 1993.Google Scholar
  3. [3]
    M.A. Bezem and J.F. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Technical Report Logic Group Preprint Series No. 88, Utrecht University, March 1993.Google Scholar
  4. [4]
    M.A. Bezem and J.F. Groote. Invariants in process algebra with data. Technical Report Logic Group Preprint Series No. 98, Utrecht University, September 1993.Google Scholar
  5. [5]
    M.A. Bezem and J.F. Groote. A correctness proof of a one bit sliding window protocol in µCRL. To appear as technical report, Logic Group Preprint Series, Utrecht University, 1993.Google Scholar
  6. [6]
    M.A. Bezem and J.F. Groote. A correctness proof of a sliding window protocol in µCRL. To appear as technical report, Logic Group Preprint Series, Utrecht University, 1993.Google Scholar
  7. [7]
    D. van Dalen. Logic and Structure. Springer-Verlag, 1983.Google Scholar
  8. [8]
    G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. PaulinMohring, and B. Werner. The Coq proof assistant user’s guide. Version 5. 8. Technical report, INRIA — Rocquencourt, May 1993.Google Scholar
  9. [9]
    W.J. Fokkink. A simple specification language combining processes, time and data. Technical Report CS-R9132, CWI, Amsterdam, 1991.Google Scholar
  10. [10]
    J.F. Groote and H. Korver. A correctness proof of the bakery protocol in µ-CRL. Technical Report 80, Logic Group Preprint Series, Utrecht University, 1992.Google Scholar
  11. [11]
    J.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large data packets. To appear as Technical Report, Logic Group Preprint Series, Utrecht University, 1993.Google Scholar
  12. [12]
    J.F. Groote and A. Ponse. The syntax and semantics of pCRL. Report CS-R9076, CWI, Amsterdam, 1990.Google Scholar
  13. [13]
    J.F. Groote and A. Ponse. Proof theory for µCRL. Report CS-R9138, CWI, 1991.Google Scholar
  14. [14]
    C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, 1985.MATHGoogle Scholar
  15. [15]
    C.A.R. Hoare, I.J. Hayes, He Jifeng, C.C. Morgan, A.W. Roscoe, J.W. Sanders, I.H. Sorensen, J.M. Spivey, and B.A. Sufrin. Laws of programming. Communications of the ACM, 30 (8): 672–686, August 1987.MATHCrossRefGoogle Scholar
  16. [16]
    G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International, 1991.Google Scholar
  17. [17]
    H. Korver and J. Springintveld. A computer-checked verification of Milner’s scheduler. Technical report, CWI, Amsterdam, 1993. To Appear.Google Scholar
  18. [18]
    R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.MATHGoogle Scholar
  19. [19]
    A. Ponse. Computable processes and bisimulation equivalence. Report CS-R9207, CWI, Amsterdam, January 1992.Google Scholar
  20. [20]
    M.P.A. Sellink. Verifying process algebra proofs in type theory. Technical Report Logic Group Preprint Series No. 87, Utrecht University, March 1993.Google Scholar
  21. [21]
    R. de Simone and D. Vergamini. Aboard AUTO. Technical Report 111, INRIA, Centre Sophia-Antipolis, Valbonne Cedex, 1989.Google Scholar
  22. [22]
    A.S. Troelstra and D. van Dalen. Constructivism in Mathematics, An Introduction (vol I). North-Holland, 1988.Google Scholar

Copyright information

© British Computer Society 1994

Authors and Affiliations

  • Jan Friso Groote
    • 1
  • Alban Ponse
    • 2
  1. 1.Department of PhilosophyUtrecht UniversityUtrechtThe Netherlands
  2. 2.Dep. of Mathematics and Computer ScienceUniversity of AmsterdamAmsterdamThe Netherlands

Personalised recommendations