Skip to main content
SpringerLink
Log in
Book cover

International Conference on Concurrency Theory

CONCUR 1990: CONCUR '90 Theories of Concurrency: Unification and Extension pp 141–151Cite as

A preorder for partial process specifications

  • Selected Presentations
  • Conference paper
  • First Online:

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

Abstract

This paper presents a behavioral preorder for relating partial process specifications to implementations and establishes that it is “adequate” in the following sense: one specification may be used to characterize all implementations of a network component that are correct for any network context exhibiting a particular interface. This property makes the preorder particularly suitable for reasoning compositionally about networks of processes. The paper also gives a sound and complete axiomatization for finite processes of the largest precongruence contained in this new preorder.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abramsky, S. “Observation Equivalence as a Testing Equivalence.” Theoretical Computer Science, v. 53, 1987, pp. 225–241.

    Google Scholar 

  2. Cleaveland, R., J. Parrow and B.U. Steffen. “A Semantics-Based Tool for the Verification of Finite-State Systems.” In Proceedings of the Ninth IFIP Symposium on Protocol Specification, Testing and Verification, June 1989. To be published by North-Holland.

    Google Scholar 

  3. Cleaveland, R., J. Parrow and B.U. Steffen. “The Concurrency Workbench.” In Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science 407. Springer-Verlag, Berlin, 1989.

    Google Scholar 

  4. Cleaveland, R. and B. Steffen. “When is ‘Partial’ Adequate? A Logic-Based Proof Technique for Partial Specifications.” In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, pp. 108–117. Computer Society Press, Los Alamitos, 1990.

    Google Scholar 

  5. Graf, S. and B. Steffen. “Using Interface Specifications for Compositional Reduction.” To appear in Proceedings of the Workshop on Computer-Aided Verification.

    Google Scholar 

  6. Larsen, K.G., and R. Milner. “Verifying a Protocol Using Relativized Bisimulation.” In Proceedings of ICALP 87, Lecture Notes in Computer Science 267. Springer-Verlag, Berlin.

    Google Scholar 

  7. Larsen, K.G., and B. Thomsen. “Compositional Proofs by Partial Specification of Processes.” Technical Report 87-20, University of Aalborg, July 1987.

    Google Scholar 

  8. Larsen, K.G. and B. Thomsen. “A Modal Process Logic.” In Proceedings of the Third Annual Symposium on Logic in Computer Science, pp. 203–210. Computer Society Press, Washington DC, 1988.

    Google Scholar 

  9. Larsen, K. and Xinxin, L. “Equation Solving through an Operational Semantics of Context.” In Proceedings of the Fifth Annual Symposium on Logic in Computer Sicence, pp. 108–117. Computer Society Press, Los Alamitos, 1990.

    Google Scholar 

  10. Milner, R. A Calculus of Communicating Systems. Lecture Notes in Computer Science 92. Springer-Verlag, Berlin, 1980.

    Google Scholar 

  11. Milner, R. “A Modal Characterization of Observable Machine Behaviour.” Lecture Notes in Computer Science 112, pp. 25–34. Springer-Verlag, Berlin, 1981.

    Google Scholar 

  12. Milner, R. Communication and Concurrency. Prentice-Hall, New York, 1989.

    Google Scholar 

  13. Shurek, G. and O. Grumberg. “The Modular Framework of Computer-Aided Verification: Motivation, Solutions and Evaluation Criteria.” To appear in Proceedings of the Workshop on Computer-Aided Verification.

    Google Scholar 

  14. Steffen, B.U. “Characteristic Formulae for CCS with Divergence.” In Proceedings of Eleventh International Colloquium on Automata, Languages and Programming, 1989.

    Google Scholar 

  15. Stirling, C. “Modal Logics for Communicating Systems.” Theoretical Computer Science, v. 49, 1987, pp. 311–347.

    Google Scholar 

  16. Walker, D. “Bisimulations and Divergence.” In Proceedings of the Third Annual Symposium on Logic in Computer Science, pp. 186–192. Computer Society Press, Washington DC, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, North Carolina State University, Box 8206, 27695-8206, Raleigh, NC, USA

    Rance Cleaveland

  2. Department of Computer Science, Aarhus University, Ny Munkegade 116, DK 8000, Aarhus C, Denmark

    Bernhard Steffen

Authors
  1. Rance Cleaveland
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernhard Steffen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. C. M. Baeten J. W. Klop

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cleaveland, R., Steffen, B. (1990). A preorder for partial process specifications. In: Baeten, J.C.M., Klop, J.W. (eds) CONCUR '90 Theories of Concurrency: Unification and Extension. CONCUR 1990. Lecture Notes in Computer Science, vol 458. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0039057

Download citation

  • DOI: https://doi.org/10.1007/BFb0039057

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-53048-0

  • Online ISBN: 978-3-540-46395-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation