Abstract
The aim of this work is to investigate mechanical support for process algebra, both for concrete applications and theoretical properties. Two approaches are presented using the verification system PVS. One approach declares process terms as an uninterpreted type and specifies equality on terms by axioms. This is convenient for concrete applications where the rewrite mechanisms of PVS can be exploited. For the verification of theoretical results, often induction principles are needed. They are provided by the second approach where process terms are defined as an abstract datatype with a separate equivalence relation.
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
G. J. Akkerman and J. C. M. Baeten. Term rewriting analysis in process algebra. CWI Quarterly, 4(4):257–267, 1991.
J. C. M. Baeten and C. Verhoef. Concrete process algebra. In S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 4, Semantic Modelling, pages 149–268. Oxford University Press, Oxford, UK, 1995.
J. C. M. Baeten and W. P. Weijland. Process Algebra. Prentice-Hall, 1990.
J. A. Bergstra, I. Bethke, and A. Ponse. Process algebra with iteration and nesting. The Computer Journal, 37(4):241–258, 1994.
M. A. Bezem, R. N. Bol, and J. F. Groote. Formalizing process algebraic verifications in the calculus of constructions. Formal Aspects of Computing, 9(1):1–48, 1997.
A. Camilleri. A Higher Order Logic mechanization of the CSP failure-divergence semantics. In Proc. IV Higher Order Workshop, pages 123–150. Workshops in Computing, Springer-Verlag, 1991.
A. Camilleri, P. Inverardi, and M. Nesi. Combining interaction and automation in process algebra verification. In TAPSOFT’91, pages 283–296. LNCS 494, Springer-Verlag, 1991.
R. Cleaveland, J. Gada, P. Lewis, S. Smolka, O. Sokolsky, and S. Zhang. The Concurrency Factory-practical tools for specification, simulation, verification, and implementation. In Proc. DIMACS Workshop on Specification of Parallel Algorithms, 1994.
R. Groenboom, C. Hendriks, I. Polak, J. Terlouw, and J. T. Udding. Algebraic proof assistants in HOL. In Mathematics of Program Construction, pages 304–321. LNCS 947, Springer-Verlag, 1995.
J. F. Groote, F. Monin, and J. Springintveld. A computer checked algebraic verification of a distributed summation algorithm. Computing Science Report 97/14, Eindhoven University of Technology, The Netherlands, 1997.
H. Korver and A. Sellink. On automating process algebra proofs. In Proc. Symp. on Computer and Information Sciences, ISCIS XI, volume II, pages 815–826, 1996.
H. Lin. PAM: A process algebra manipulator. In Proc. Third Workshop on Computer Aided Verification, pages 136–146. LNCS 575, Springer-Verlag, 1991.
S. Mauw and G. J. Veltink. A proof assistant for PSF. In Proc. Third Workshop on Computer Aided Verification, pages 158–168. LNCS 575, Springer-Verlag, 1991.
T. F. Melham. A mechanized theory of the π-calculus in HOL. Technical Report 244, Computer Laboratory, University of Cambridge, 1992.
M. Nesi. Value-passing CCS in HOL. In Proc. 6th Workshop on Higher Order Logic Theorem Proving and Applications, pages 352–365. LNCS 780, Springer-Verlag, 1993.
S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, 1995.
L. C. Paulson. Isabelle: A Generic Theorem Prover. LNCS 828, Springer-Verlag, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basten, T., Hooman, J. (1999). Process Algebra in PVS. In: Cleaveland, W.R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1999. Lecture Notes in Computer Science, vol 1579. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49059-0_19
Download citation
DOI: https://doi.org/10.1007/3-540-49059-0_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65703-3
Online ISBN: 978-3-540-49059-3
eBook Packages: Springer Book Archive