Summary
A process P satisfies a specification S if every observation we can make of the behaviour of P is allowed by S. We use this idea of process correctness as a starting point for developing a specific form of denotational semantics for processes, called here specification — oriented semantics. This approach serves as a uniform framework for generating and relating a series of increasingly sophisticated denotational models for Communicating Processes.
These models differ in the underlying structure of their observations which influences both the number of representable language operators and the induced notion of process correctness. Safety properties are treated by all models; the more sophisticated models also permit proofs of certain liveness properties. An important feature of the models is a special hiding operator which abstracts from internal process activity. This allows large processes to be composed hierarchically from networks of smaller ones in such a way that proofs of the whole are constructed from proofs of its components. We also show the consistency of our denotational models w.r.t. a simple operational semantics based on transitions which make internal process activity explicit.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM TOPLAS 2, 359–385 (1980)
Apt, K.R.: Formal justification of a proof system for communicating sequential processes. J. Assoc. Comput. Mach. 30, 197–216 (1983)
de Bakker, J.W.: Mathematical theory of program correctness. London: Prentice Hall 1980
de Bakker, J.W., Bergstra, J.A., Klop, J.W., Meyer, J.-J.C.: Linear time and branching time semantics for recursion with merge. TCS 34, 134–156 (1984)
de Bakker, J.W., Meyer, J.-J.C., Olderog, E.-R.: Infinite streams and finite observations in the semantics of uniform concurrency. In: Proc. 12th Coll. Automata, Languages and Programming. (W. Brauer ed.). Lect. Notes Comput. Sci. 194, 149–157 (1985)
de Bakker, J.W., Meyer, J.-J.C., Olderog, E.-R., Zucker, J.I.: Transition systems, infinitary languages and the semantics of uniform concurrency. In: Proc. 17th ACM Symposium on Theory of Computing, pp. 252–262. Providence 1985
de Bakker, J.W., Zucker, J.I.: Processes and the denotational semantics of concurrency. Inf. Control 54, 70–120 (1982)
Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. TCS 37, 77–121 (1985)
Bergstra, J.A., Klop, J.W., Olderog, E.-R.: Readies and failures in the algebra of communicating processes. Report CS-R8523, Center for Mathematics and Computer Science, Amsterdam 1985
Brock, J.D., Ackermann, W.B.: Scenarios: a model for nondeterminate computations. In: Formalisation of Programming Concepts (J. Diaz, I. Ramos, eds.). Lect. Notes Comput. Sci. 107, 252–267 (1981)
Brookes, S.D.: A model for communicating sequential processes. D. Phil. Thesis, Oxford Univ. 1983
Brookes, S.D.: On the relationship of CCS and CSP. In: Proc. 10th Coll. Automata, Languages and Programming (J. Diaz, ed.). Lect. Notes Comput. Sci. 154, 83–96 (1983)
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. Assoc. Comput. Mach. 31, 560–599 (1984)
Brookes, S.D., Roscoe, A.W.: An improved failures model for communicating sequential processes. In: Proc. NSF-SERC Seminar on Concurrency. Lect. Notes Comput. Sci. 197, 281–305 (1985)
Broy, M.: Fixed point theory for communication and concurrency. In: Formal Description of Programming Concepts II (D. Bjørner, ed.), pp. 125–146. Amsterdam: North Holland 1983
Chaochen, Z., Hoare, C.A.R.: Partial correctness of communicating processes. In: Proc. 2nd International Conference on Distributed Computing Systems. Paris 1981
Francez, N., Hoare, C.A.R., Lehmann, D.J., de Roever, W.P.: Semantics of nondeterminism, concurrency and communication. J. Comput. Syst. Sci. 19, 290–308 (1979)
Francez, N., Lehmann, D., Pnueli, A.: A linear history semantics for languages for distributed programming. TCS 32, 25–46 (1984)
Goguen, J.A., Thatcher, J.W., Wagner, E.G., Wright, J.B.: Initial algebra semantics and continuous algebras. J. Assoc. Comput. Mach. 24, 68–95 (1977)
Guessarian, I.: Algebraic semantics. Lect. Notes Comput. Sci. 99 (1981)
Hehner, E.C.R.: Predicative programming, Part I and II. Commun. ACM 27, 134–151 (1984)
Hehner, E.C.R., Hoare, C.A.R.: A more complete model of communicating processes. TCS 26, 105–120 (1983)
Hennessy, M.: Acceptance trees. J. Assoc. Comput. Mach. 32, 896–928 (1985)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach. 32, 137–161 (1985)
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21, 666–677 (1978)
Hoare, C.A.R.: A model for communicating sequential processes. In: On the Construction of Programs (R.M. McKeag, A.M. McNaghton, eds.), pp. 229–243. Cambridge: University Press 1980
Hoare, C.A.R.: A calculus of total correctness for communicating processes. Sci. Comput. Program. 1, 49–72 (1981)
Hoare, C.A.R.: Specifications, programs and implementations. Tech. Monograph PRG-29, Progr. Research Group. Oxford University 1982
Hoare, C.A.R.: Communicating sequential processes. London: Prentice Hall 1985
INMOS: OCCAM programming manual. London: Prentice Hall 1984
Jorrand, P.: Specification of communicating processes and process implementation correctness. In: Proc. 5th Intern. Symp. on Programming. (M. Dezani-Ciancaglini, U. Montanari, eds.). Lect. Notes Comput. Sci. 137, 242–256 (1983)
Keller, R.: Formal verification of parallel programs. Commun. ACM 19, 371–384 (1976)
Levin, G.M., Gries, D.: A proof technique for communicating sequential processes. Acta Inf. 15, 281–302 (1981)
Milner, R.: A calculus of communicating systems. Lect. Notes Comput. Sci. 92 (1980)
Milner, R.: A modal characterisation of observable machine-behaviour. In: Proc. 6th Coll. Trees in Algebra and Programming (E. Asteriano, C. Böhm, eds.). Lect. Notes Comput. Sci. 112, 25–34 (1981)
Milner, R.: Calculi for synchrony and asynchrony. TCS 25, 267–310 (1983)
Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7, 417–426 (1981)
Misra, J., Chandy, K.M., Smith, T.: Proving safety and liveness of communicating processes with examples. In: Proc. 1st ACM SIGACT-SIGOPS Symp. Principles of Distributed Computing, pp. 201–208. Ottawa 1982
de Nicola, R.: A complete set of axioms for a theory of communicating sequential processes. In: Proc. Intern. Conf. on Foundations of Computation Theory (M. Karpinski, ed.). Lect. Notes Comput. Sci. 158, 115–126 (1983)
de Nicola, R., Hennessy, M.: Testing equivalences for processes. TCS 34, 83–134 (1984)
Olderog, E.-R.: Specification-oriented programming in TCSP. In: Logics and Models of Concurrent Systems (K.R. Apt, ed.), pp. 397–435. Berlin, Heidelberg, New York: Springer 1985
Olderog, E.-R., Hoare, C.A.R.: Specification-oriented semantics for communicating processes (preliminary version). In: Proc. 10th Coll. Automata, Languages and Programming (J. Diaz, ed.). Lect. Notes Comput. Sci. 154, 561–572 (1983)
Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM TOPLAS 4, 455–495 (1982)
Plotkin, G.D.: An operational semantics for CSP. In: Formal Description of Programming Concepts II (D. Bjørner, ed.), pp. 199–223. Amsterdam: North Holland 1983
Reinecke, R.: Networks of communicating processes: a functional implementation. Manuscript, Dept. Comput. Sci., Univ. of Kaiserslautern 1983
Roscoe, A.W.: A mathematical theory of communicating processes. D. Phil., Thesis, Oxford Univ. 1982
Rounds, W.C., Brookes, S.D.: Possible futures, acceptances, refusals and communicating processes. In: Proc. 22nd IEEE Symp. on Foundations of Computer Science, Nashville, Tennessee 1981
Smyth, M.B.: Power domains. J. Comput. Syst. Sci. 16, 23–26 (1978)
Soundararajan, N., Dahl, O.-J.: Partial correctness semantics of communicating sequential processes. Research Rep. No. 66, Inst. of Informatics, Univ. of Oslo 1982
Stoy, J.E.: Denotational semantics: the Scott-Strachey approach to programming language theory. Cambridge: MIT Press 1977
Winskel, G.: Events in computation. Ph. D. Thesis, Dept. Comput. Sci., Univ. of Edinburgh 1980
Zwiers, J., de Roever, W.P., van Emde Boas, P.: Compositionality and concurrent networks. In: Proc. 12th Coll. Automata, Languages and Programming (W. Brauer, ed.). Lect. Notes Comput. Sci. 194, 509–519 (1985)
Author information
Authors and Affiliations
Additional information
A preliminary version of this paper appeared in [42]
Rights and permissions
About this article
Cite this article
Olderog, E.R., Hoare, C.A.R. Specification-oriented semantics for Communicating Processes. Acta Informatica 23, 9–66 (1986). https://doi.org/10.1007/BF00268075
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00268075