Abstract
Most existing verification tools for process algebras allow the correctness of specifications to be checked in a fully automatic fashion. These systems have the obvious advantage of being easy to use, but unfortunately they also have some drawbacks. In particular, they do not always succeed in completing the verification analysis, due to the problem of state explosion, and they do not provide any insight into the meaning of the intended specifications. In this paper we consider an alternative approach in which both interactive and automatic techniques are combined in the hope that the advantages of automation are retained, and that some of its disadvantages are overcome. To achieve our goal, we use the interactive theorem prover hol as a framework for supporting the theory of observational congruence of ccs, and provide a set of automatic proof tools, based on the algebraic axiomatization of the language, which can be used interactively. To illustrate how interaction and automation can be intermixed, we describe two verification strategies which exhibit different degrees of user interaction.
Research supported by, and collaboratively carried out at, Hewlett-Packard Laboratories, Pisa Science Centre, Corso Italia 115, I-56125 Pisa, Italy.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Bolognesi T., Caneve M., 'squiggles—A Tool for the Analysis of lotos Specifications', in Formal Description Techniques, K. Turner (ed.), North-Holland, 1989.
Camilleri A. J., ‘Mechanizing Csp Trace Theory in Higher Order Logic', IEEE Transactions on Software Engineering, Special Issue on Formal Methods, N. G. Leveson (ed.), September 1990, Vol. 16, No. 9., pp. 993–1004.
Camilleri A. J., ‘A Higher Order Logic Mechanization of the csp Failure-Divergence Semantics', in proceedings of the 4th Higher Order Workshop, Banff, Springer-Verlag (to appear).
Church A., ‘A Formulation of the Simple Theory of Types', The Journal of Symbolic Logic, 1940, Vol. 5, pp. 56–68.
Cleaveland R., Panangaden P., ‘Type Theory and Concurrency', International Journal of Parallel Programming, November 1988, Vol. 12, No. 2, pp. 153–206.
Cleaveland R., Parrow J., Steffen B., ‘The Concurrency Workbench: Operating Instructions', Technical Note LFCS-TN-10, University of Edinburgh, Laboratory for the Foundations of Computer Science, September 1988.
Cousineau G., Huet G., Paulson L., ‘The ml Handbook', INRIA, 1986.
Davies J., ‘Assisted Proofs for Communicating Sequential Processes', M.Sc. Dissertation, Oxford University Computer Laboratory, Programming Research Group, September 1987.
De Nicola R., Hennessy M. C., ‘Testing Equivalence for Processes', Journal of Theoretical Computer Science, 1983, Vol. 34, pp. 83–133.
De Nicola R., Inverardi P., Nesi M., ‘Using Axiomatic Presentation of Behavioural Equivalences for Manipulating ccs Specifications', Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, June 12–14, 1989, Lecture Notes in Computer Science, Springer-Verlag, 1990, Vol. 407, pp. 54–67.
De Simone R., Vergamini D., ‘Aboard AUTO', Technical Report 111, INRIA, 1989.
Fernandez J., C., ‘Aldebaran: Un système de vérification par réduction de processus communicants', Ph.D. Thesis, Université de Grenoble, 1988.
van Glabbeek R.J., Weijland W.P., ‘Branching Time and Abstraction in Bisimulation Semantics', Proceedings of the IFIP 11th World Computer Congress, San Francisco, 1989.
Godskesen J.C., Larsen K.G., Zeeberg M., ‘TAV Users Manual', Internal Report, Ålborg University Centre, Denmark, 1989.
Gordon M. J. C., ‘hol—A Proof Generating System for Higher-Order Logic', in VLSI Specification, Verification and Synthesis, Birtwistle G. and Subrahmanyam P. A. (eds.), Kluwer Academic Publishers, Boston, 1988, pp. 73–128, Proceedings of the Hardware Verification Workshop, Calgary, Canada, 12–16 January 1987.
Gordon M. J. C., ‘Mechanizing Programming Logics in Higher Order Logic', in Current Trends in Hardware Verification and Automated Theorem Proving, Birtwistle G., Subrahmanyam P. (eds.), Springer-Verlag, 1989, pp. 387–439, Proceedings of the Banff Workshop on Hardware Verification, Banff, Canada, 1988.
Gordon M., Melham T., ‘Mechanizing the II-calculus in hol', Private Communication, 1990.
Graf S., Steffen B., ‘Compositional Minimization of Finite State Processes’ Proceedings of the Workshop on Computer-Aided Verification, New Brunswick, New Jersey, June 1990.
Inverardi P., Nesi M., ‘A Rewriting Strategy to Verify Observational Congruence', Information Processing Letters, 1990, Vol. 35, pp. 191–199.
Inverardi P., Nesi M. ‘Deciding Observational Congruence of Finite-State ccs Expressions by Rewriting', Internal Report B4-10, Istituto di Elaborazione dell' Informazione, C. N. R., March 1990.
Lin H., ‘A Process Algebra Manipulator', Technical Report, University of Sussex Computer Laboratory, (to appear).
Melham T. F., ‘Automating Recursive Type Definitions in Higher Order Logic', in Current Trends in Hardware Verification and Automated Theorem Proving, Birtwistle G., Subrahmanyam P. (eds.), Springer-Verlag, 1989, pp. 341–386, Proceedings of the Banff Workshop on Hardware Verification, Banff, Canada, 1988.
Milner R., Communication and Concurrency, Prentice-Hall Int., 1989.
Paulson L. C., Logic and Computation—Interactive Proof with Cambridge lcf, Cambridge Tracts in Theoretical Computer Science (2), Cambridge University Press, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Camilleri, A., Inverardi, P., Nesi, M. (1991). Combining interaction and automation in process algebra verification. In: Abramsky, S., Maibaum, T.S.E. (eds) TAPSOFT '91. TAPSOFT 1991. Lecture Notes in Computer Science, vol 494. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540539816_72
Download citation
DOI: https://doi.org/10.1007/3540539816_72
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53981-0
Online ISBN: 978-3-540-46499-0
eBook Packages: Springer Book Archive