Proof Theory for µCRL: A Language for Processes with Data.
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.
Unable to display preview. Download preview PDF.
- J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.Google Scholar
- J.A. Bergstra, I. Bethke, and A. Ponse. Process algebra with combinators. Report P9319, Programming Research Group, University of Amsterdam, 1993.Google Scholar
- 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
- 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
- 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
- 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
- D. van Dalen. Logic and Structure. Springer-Verlag, 1983.Google Scholar
- 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
- W.J. Fokkink. A simple specification language combining processes, time and data. Technical Report CS-R9132, CWI, Amsterdam, 1991.Google Scholar
- 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
- 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
- J.F. Groote and A. Ponse. The syntax and semantics of pCRL. Report CS-R9076, CWI, Amsterdam, 1990.Google Scholar
- J.F. Groote and A. Ponse. Proof theory for µCRL. Report CS-R9138, CWI, 1991.Google Scholar
- G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International, 1991.Google Scholar
- H. Korver and J. Springintveld. A computer-checked verification of Milner’s scheduler. Technical report, CWI, Amsterdam, 1993. To Appear.Google Scholar
- A. Ponse. Computable processes and bisimulation equivalence. Report CS-R9207, CWI, Amsterdam, January 1992.Google Scholar
- 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
- R. de Simone and D. Vergamini. Aboard AUTO. Technical Report 111, INRIA, Centre Sophia-Antipolis, Valbonne Cedex, 1989.Google Scholar
- A.S. Troelstra and D. van Dalen. Constructivism in Mathematics, An Introduction (vol I). North-Holland, 1988.Google Scholar