Abstract
A process algebra and readiness specifications introduced by Olderog are extended to a framework in which processes parameterized with other processes can be specified, defined and verified. Higher order process-parameters are allowed. The formalism resembles typed lambda calculus built on top of a process algebra, where specifications play the role of types. A proof system for deriving judgements “parametric process meets a specification” is given.
This work was partially supported by the following grants: KBN Grant No. PB-1312/P3/92/02, CRIT IC 1010/II, and (in case of the second author) ESPRIT BRA CONCUR2.
Preview
Unable to display preview. Download preview PDF.
References
H.P. Barendregt, Lambda Calculi with Types, in: Handbook of Logic in Computer Science, vol. 2 (S. Abramsky, Dov M. Gabbay, T. S. E. Maibaum, Eds.) pp. 117–309, Calderon Press, Oxford 1992.
S. Holmström, A refinement calculus for specification in Hennessy-Milner logic with recursion, Formal Aspects of Computing, vol. 1 (3). pp. 242–272, 1989.
K. Larsen and R. Milner, A Complete Protocol Verification using Relativised Bisimulations, R 86-12, Institute of Electrical Systems, Aalborg University Centre, 1986. 4. R. Milner, Communication and Concurency, Prentice Hall, 1989.
E.-R. Olderog, Nets, Terms and Formulas, Cambridge University Press, Cambridge 1991.
E.-R. Olderog, Towards a design calculus for communicating programs, in: Proc. CONCUR '91, LNCS, Springer, 1991.
W. Pawłowski, P. Paczkowski, S. Sokołowski, A specification system for parametric concurrent processes, electronically available as ftp://ipipan.gda.pl/pub/ local-users/Pawlowski-W./parametric.ps.gz.
S. Sokołowski, Requirement specifications and their realizations: toward a unified framework. Submitted to Theoretical Computer Science. A preliminary version has appeared as: The GDM approach to specifications and their realizations. Part I: Specification systems. ICS PAS Report 797, Warszawa 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pawłowski, W., Paczkowski, P., Sokołowski, S. (1996). Specifying and verifying parametric processes. In: Penczek, W., Szałas, A. (eds) Mathematical Foundations of Computer Science 1996. MFCS 1996. Lecture Notes in Computer Science, vol 1113. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61550-4_171
Download citation
DOI: https://doi.org/10.1007/3-540-61550-4_171
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61550-7
Online ISBN: 978-3-540-70597-0
eBook Packages: Springer Book Archive