Abstract
Value-passing ccs is a process algebra in which actions consist of sending and receiving values through communication ports, and the transmitted data can be tested using a conditional construct. In a previous work, a verification environment for pure ccs agents (no value-passing, only synchronization) has been mechanized in the hol system. This paper presents an embedding of value-passing ccs in hol that translates value-passing agents into pure ones. Once the translation has been defined, the hol verification environment for pure ccs is used to derive a proof environment for the value-passing calculus.
The research described in this paper has been partially supported by Girton College, Cambridge.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Bruns, G., ‘A language for value-passing CCS', Technical Report ECS-LFCS-91-175, LFCS, University of Edinburgh, August 1991.
Camilleri, J. and T. Melham, ‘Reasoning with Inductively Defined Relations in the hol Theorem Prover', Technical Report No. 265, Computer Laboratory, University of Cambridge, August 1992.
Cleaveland, R., J. Parrow, and B. Steffen, ‘The Concurrency Workbench', in, pp. 24–37.
Gordon, M. J. C. and T. F. Melham, ‘Introduction to hol: a theorem proving environment for higher order logic', Cambridge University Press, 1993.
Gunter, E. L., ‘Why We Can't Have SML Style datatype Declarations in hol', in Proceedings of the 1992 International Workshop on Higher Order Logic Theorem Proving and Its Applications, L. J. M. Claesen and M. J. C. Gordon (eds.), IFIP Transactions A-20, North-Holland, 1993, pp. 561–568.
Hennessy, M., ‘A Proof System for Communicating Processes with Value-Passing', in Formal Aspects of Computing, Vol. 3, 1991, pp. 346–366.
Hennessy, M. and H. Lin, 'symbolic bisimulations', Technical Report 1/92, Computer Science, University of Sussex, April 1992.
Hennessy, M. and H. Lin, ‘Proof Systems for Message-Passing Process Algebras', Technical Report 5/93, Computer Science, University of Sussex, February 1993, also in Proceedings of CONCUR '93, E. Best (ed.), Lecture Notes in Computer Science, Springer-Verlag, Vol. 715, 1993.
Lin, H., ‘A Verification Tool for Value-Passing Processes', in Proceedings of PSTV XIII, Liege, Belgium, May 1993.
Melham, T. F., ‘Automating Recursive Type Definitions in Higher Order Logic', in Current Trends in Hardware Verification and Automated Theorem Proving, G. Birtwistle and P. Subrahmanyam (eds.), Springer-Verlag, 1989, pp. 341–386.
Melham, T. F., ‘A Mechanized Theory of the π-calculus in hol', Technical Report No. 244, Computer Laboratory, University of Cambridge, January 1992.
Melham, T. F., ‘A Package for Inductive Relation Definitions in hol', in Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, P. J. Windley, M. Archer, K. N. Levitt and J. J. Joyce (eds.), IEEE Computer Society Press, 1992, pp. 350–357.
Milner, R., Communication and Concurrency, Prentice Hall, London, 1989.
Nesi, M., ‘A Formalization of the Process Algebra ccs in Higher Order Logic', Technical Report No. 278, Computer Laboratory, University of Cambridge, December 1992.
Nesi, M., ‘Formalizing a Modal Logic for ccs in the hol Theorem Prover', in Proceedings of the 1992 International Workshop on Higher Order Logic Theorem Proving and Its Applications, L. J. M. Claesen and M. J. C. Gordon (eds.), IFIP Transactions A-20, North-Holland, 1993, pp. 279–294.
Shepherd, D. E., Private communication, March 1993.
Taubner, D., ‘A note on the notation of recursion in process algebras', Information Processing Letters, North-Holland, 1991, Vol. 37, pp. 299–303.
Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, 1989, J. Sifakis (ed.), Lecture Notes in Computer Science, Springer-Verlag, Vol. 407, 1990.
Proceedings of the 2nd Workshop on Computer Aided Verification, New Brunswick, New Jersey, 1990, E. M. Clarke and R. P. Kurshan (eds.), Lecture Notes in Computer Science, Springer-Verlag, Vol. 531, 1991.
Proceedings of the 3rd Workshop on Computer Aided Verification, Ã…lborg University, 1991, K. G. Larsen and A. Skou (eds.), Lecture Notes in Computer Science, Springer-Verlag, Vol. 575, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nesi, M. (1994). Value-passing CCS in HOL. In: Joyce, J.J., Seger, CJ.H. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1993. Lecture Notes in Computer Science, vol 780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57826-9_147
Download citation
DOI: https://doi.org/10.1007/3-540-57826-9_147
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57826-0
Online ISBN: 978-3-540-48346-5
eBook Packages: Springer Book Archive