Specification-oriented semantics for communicating processes

  • E. -R. Olderog
  • C. A. R. Hoare
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)


We are aiming at a classification of semantical models for Communicating Processes that will enable us to recommend certain models which are just detailed enough for particular applications. But before such an aim can be fully realised, more sophisticated models of processes should be studied.

For example, we have not considered the notion of state so far. This would allow to add assignment and explicit value passing between processes, thus combining sequential programs with Communicating Processes.

It is also important to ensure that the operators satisfy the usual algebraic laws, for example parallel composition should be associative. And the relationship between specification-oriented denotational semantics used here and the operational semantics used in [12,13,16] should be studied. This requires an explicit concept of divergence. In particular, it is interesting to investigate how the criterion P sat S can be derived systematically from the operational semantics. A significant step in this direction has already been made in [14].

Finally, an explicit syntax for specifications and proof systems for the relation P sat S should be developed. First proposals for such proof systems can be found in [5,9].


Semantical Model Operational Semantic Proof System Concurrent Program Denotational Semantic 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    J.W. de Bakker, Mathematical Theory of Program Correctness (Prentice Hall, London, 1980).Google Scholar
  2. [2]
    J.W. de Bakker, J.I. Zucker, Denotational semantics of concurrency, in: Proc. 14th ACM Symp. on Theory of Computing (1982) 153–158.Google Scholar
  3. [3]
    J.D. Brock, W.B. Ackermann, Scenarios: a model for nondeterminate computations, in: J. Diaz, I. Ramos, Eds., Formalisation of Programming Concepts, LNCS 107 (Springer, Berlin-Heidelberg-New York, 1981) 252–267.Google Scholar
  4. [4]
    M. Broy, Fixed point theory for communication and concurrency, in: D. BjØrner, Ed., Formal Description of Programming Concepts II, Preliminary Proc. IFIP TC-2 Working Conference (North Holland, Amsterdam, 1982) 104–126.Google Scholar
  5. [5]
    Z. Chaochen, C.A.R. Hoare, Partial correctness of communicating processes, in: Proc. 2nd International Conference on Distributed Computing Systems, Paris (1981).Google Scholar
  6. [6]
    N. Francez, C.A.R. Hoare, D.J. Lehmann, W.P. de Roever, Semantics of nondeterminism, concurrency and communication, JCSS 19 (1979) 290–308.Google Scholar
  7. [7]
    E.C.R. Hehner, C.A.R. Hoare, A more complete model of communicating processes (to appear in Theoret. Comp. Sci.) 1982.Google Scholar
  8. [8]
    C.A.R. Hoare, A model for communicating sequential processes, in: R.M, McKeag, A.M. McNaghton, Eds., On the Construction of Programs (Cambridge University Press, 1980) 229–243.Google Scholar
  9. [9]
    C.A.R. Hoare, A calculus of total correctness for communicating processes, Sci. Comp. Programming 1 (1981) 49–72.Google Scholar
  10. [10]
    C.A.R. Hoare, Specifications, programs and implementations, Tech. Monograph PRG-29, Oxford Univ., Progr. Research Group, Oxford 1982.Google Scholar
  11. [11]
    C.A.R. Hoare, S.D. Brookes, A.W. Roscoe, A theory of communicating sequential processes, Tech. Monograph PRG-16, Oxford Univ., Progr. Research Group, Oxford 1981.Google Scholar
  12. [12]
    R. Milner, A calculus of communicating systems, LNCS 92 (Springer, Berlin-Heidelberg-New York, 1980).Google Scholar
  13. [13]
    R. Milner, Four combinators for concurrency, in: Proc. ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computations, Ottawa, 1982.Google Scholar
  14. [14]
    R. de Nicola, M.C.B. Hennessy, Testing equivalences for processes, Internal Report CSR-123-82, Univ. of Edinburgh, Computer Science Dept., 1982.Google Scholar
  15. [15]
    S. Owicki, L. Lamport, Proving liveness properties of concurrent programs, ACM TOPLAS 4 (1982) 455–495.Google Scholar
  16. [16]
    G.D. Plotkin, An operational semantics for CSP, in: D. BjØrner, Ed., Formal Description of Programming Concepts II, Preliminary Proc IFIP TC-2 Working Conference (North Holland, Amsterdam, 1982) 185–208.Google Scholar
  17. [17]
    D.S. Scott, Domains for denotational semantics, in: M. Nielsen, E.M. Schmidt, Eds., Proc. 9th ICALP, LNCS 140 (Springer, Berin-Heidel berg-New York, 1982) 577–613.Google Scholar
  18. [18]
    M.B. Smyth, Power domains, JCSS 16 (1978) 23–26.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • E. -R. Olderog
    • 1
    • 2
  • C. A. R. Hoare
    • 1
    • 2
  1. 1.Programming Research GroupOxford UniversityUK
  2. 2.Institut für InformatikUniversität KielDeutschland

Personalised recommendations