Skip to main content

Specifying and verifying parametric processes

  • Contributed Papers
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1996 (MFCS 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1113))

  • 154 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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.

    Google Scholar 

  2. 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.

    Article  Google Scholar 

  3. 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.

    Google Scholar 

  4. E.-R. Olderog, Nets, Terms and Formulas, Cambridge University Press, Cambridge 1991.

    Google Scholar 

  5. E.-R. Olderog, Towards a design calculus for communicating programs, in: Proc. CONCUR '91, LNCS, Springer, 1991.

    Google Scholar 

  6. 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.

    Google Scholar 

  7. 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.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Wojciech Penczek Andrzej Szałas

Rights and permissions

Reprints 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

Publish with us

Policies and ethics