Skip to main content
SpringerLink
Log in

Behavior: a temporal appreach to process modeling

  • Conference paper
  • First Online:
Logics of Programs (Logic of Programs 1985)

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

Included in the following conference series:

Abstract

This paper describes an approach to modeling processes and networks of processes that communicate exclusively through message passing. A process is defined by its set of possible behaviors, where each behavior is an abstraction of some infinite execution sequence of the process. The resulting model of processes is simple and modular and facilitates information hiding. It can describe either synchronous or asynchronous networks. It supports recursively-defined networks and can characterize liveness properties such as progress of inputs and outputs, termination and deadlock. A sound and complete temporal proof system for processes is presented. It is compositional — a specification of a network is formed naturally from specifications of its component processes. A nontrivial example, comprising a specification and correctness proof for a recursive network, is given to demonstrate the usefulness of our techniques.

This research supported by NSF under grants DCR-83-202-74 and DCR-83-123-19, and by NASA under contract NAGW419.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Apt, K.R., Ten years of Hoare's logic: a survey — Part 1, ACM TOPLAS, vol. 3, no. 4, Oct 1981, 431–483.

    Google Scholar 

  2. Barringer, H., Kuiper, R. and Pnueli, A., Now you may compose temporal logic specifications, 16th ACM Symposium on the Theory of Computing, May 1984.

    Google Scholar 

  3. Brock, J.D. and Ackerman, W.B., Scenarios: a model of non-determinate computation, International Colloquium on Formalization of Programming Concepts, April 1981.

    Google Scholar 

  4. Brookes, S.D., A semantics and proof system for communicating processes, Lecture Notes in Computer Science, vol. 164, 1984, 68–85.

    Google Scholar 

  5. Harel, D., First-order dynamic logic, Lecture Notes in Computer Science, vol. 68, 1979.

    Google Scholar 

  6. Harel, D., Kozen, D. and Parikh, R., Process logic: expressiveness, decidability and completeness, JCSS vol. 25(1982), 144–170.

    Google Scholar 

  7. Hewitt, C. and Baker, H.G., Laws for communicating parallel processes, IFIP 77, 1977, 987–992.

    Google Scholar 

  8. Hoare, C.A.R., Communicating sequential processes, Communications of the ACM, vol. 21, no. 8, Aug 1978, 666–677.

    Google Scholar 

  9. Hoare, C.A.R., Notes on communicating sequential processes, Technical Monograph PRG-33, Programming Research Group, Oxford University Computing Laboratory, Aug 1983.

    Google Scholar 

  10. Kahn, G. and MacQueen, D.B., Coroutines and networks of parallel processes, IFIP 77, 1977, 993–998.

    Google Scholar 

  11. Lamport, L., What good is temporal logic? Proceedings IFIP 1983, 657–668.

    Google Scholar 

  12. Manna, Z. and Pnueli, A., Verification of concurrent programs, Part 1: The temporal framework, Technical report STAN-CS-81-836, Stanford University, June 1981.

    Google Scholar 

  13. Manna, Z. and Pnueli, A., How to cook a temporal proof system for your pet language, 10th Annual ACM Symposium on Principles of Programming Languages, Jan 1983, 141–154.

    Google Scholar 

  14. Milner, R., A calculus of communicating systems, Lecture Notes in Computer Science, vol. 92, 1980.

    Google Scholar 

  15. Nguyen, V., A theory of processes, Ph.D. Thesis, Department of Computer Science, Cornell University (in preparation).

    Google Scholar 

  16. Nguyen, V., Gries, D. and Owicki, S., A model and temporal proof system for networks of processes, 12th ACM Symposium on Principles of Programming Languages, Jan 1985, 121–131.

    Google Scholar 

  17. Pratt, V., On the composition of processes, 9th ACM Symposium on Principles of Programming Languages, Jan 1982, 213–223.

    Google Scholar 

  18. Shapiro, E. and Takeuchi, A., Object-oriented programming in Concurrent Prolog, Journal of new generation computing, vol. 1, no. 1, 1983, 25–48.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Deptartment of Computer Science, Cornell University, 14853, Ithaca, New York

    Van Nguyen, Alan Demers & David Gries

  2. Computer Systems Laboratory, Stanford University, 94305, Stanford, California

    Susan Owicki

Authors
  1. Van Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alan Demers
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Gries
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Susan Owicki
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Rohit Parikh

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nguyen, V., Demers, A., Gries, D., Owicki, S. (1985). Behavior: a temporal appreach to process modeling. In: Parikh, R. (eds) Logics of Programs. Logic of Programs 1985. Lecture Notes in Computer Science, vol 193. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15648-8_19

Download citation

  • DOI: https://doi.org/10.1007/3-540-15648-8_19

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-15648-2

  • Online ISBN: 978-3-540-39527-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation