×

zbMATH — the first resource for mathematics

Specification-oriented semantics for communicating processes. (English) Zbl 0569.68019
A process P satisfies a specification S, abbreviated P sat S, if every observation we can make about 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 notion of correctness expressed by P sat S. Safety properties are treated by all models; the more sophisticated models also permit proofs of 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 consistency of the denotational models w.r.t. a simple operational semantics based on transitions which make internal process activity explicit.

MSC:
68N25 Theory of operating systems
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM TOPLAS 2, 359–385 (1980) · Zbl 0468.68023
[2] Apt, K.R.: Formal justification of a proof system for communicating sequential processes. J. Assoc. Comput. Mach. 30, 197–216 (1983) · Zbl 0503.68021
[3] de Bakker, J.W.: Mathematical theory of program correctness. London: Prentice Hall 1980 · Zbl 0452.68011
[4] 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) · Zbl 0985.68517
[5] 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) · Zbl 0566.68011
[6] 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
[7] de Bakker, J.W., Zucker, J.I.: Processes and the denotational semantics of concurrency. Inf. Control 54, 70–120 (1982) · Zbl 0508.68011
[8] Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. TCS 37, 77–121 (1985) · Zbl 0579.68016
[9] 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 · Zbl 0677.68089
[10] 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)
[11] Brookes, S.D.: A model for communicating sequential processes. D. Phil. Thesis, Oxford Univ. 1983
[12] 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) · Zbl 0516.68024
[13] Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. Assoc. Comput. Mach. 31, 560–599 (1984) · Zbl 0628.68025
[14] 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) · Zbl 0565.68023
[15] 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
[16] Chaochen, Z., Hoare, C.A.R.: Partial correctness of communicating processes. In: Proc. 2nd International Conference on Distributed Computing Systems. Paris 1981
[17] 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) · Zbl 0434.68066
[18] Francez, N., Lehmann, D., Pnueli, A.: A linear history semantics for languages for distributed programming. TCS 32, 25–46 (1984) · Zbl 0543.68019
[19] 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) · Zbl 0359.68018
[20] Guessarian, I.: Algebraic semantics. Lect. Notes Comput. Sci. 99 (1981) · Zbl 0474.68010
[21] Hehner, E.C.R.: Predicative programming, Part I and II. Commun. ACM 27, 134–151 (1984) · Zbl 0593.68010
[22] Hehner, E.C.R., Hoare, C.A.R.: A more complete model of communicating processes. TCS 26, 105–120 (1983) · Zbl 0513.68020
[23] Hennessy, M.: Acceptance trees. J. Assoc. Comput. Mach. 32, 896–928 (1985) · Zbl 0633.68074
[24] Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach. 32, 137–161 (1985) · Zbl 0629.68021
[25] Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21, 666–677 (1978) · Zbl 0383.68028
[26] 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
[27] Hoare, C.A.R.: A calculus of total correctness for communicating processes. Sci. Comput. Program. 1, 49–72 (1981) · Zbl 0485.68025
[28] Hoare, C.A.R.: Specifications, programs and implementations. Tech. Monograph PRG-29, Progr. Research Group. Oxford University 1982
[29] Hoare, C.A.R.: Communicating sequential processes. London: Prentice Hall 1985 · Zbl 0637.68007
[30] INMOS: OCCAM programming manual. London: Prentice Hall 1984
[31] 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)
[32] Keller, R.: Formal verification of parallel programs. Commun. ACM 19, 371–384 (1976) · Zbl 0329.68016
[33] Levin, G.M., Gries, D.: A proof technique for communicating sequential processes. Acta Inf. 15, 281–302 (1981) · Zbl 0463.68034
[34] Milner, R.: A calculus of communicating systems. Lect. Notes Comput. Sci. 92 (1980) · Zbl 0452.68027
[35] 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) · Zbl 0474.68074
[36] Milner, R.: Calculi for synchrony and asynchrony. TCS 25, 267–310 (1983) · Zbl 0512.68026
[37] Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7, 417–426 (1981) · Zbl 05341575
[38] 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
[39] 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) · Zbl 0517.68027
[40] de Nicola, R., Hennessy, M.: Testing equivalences for processes. TCS 34, 83–134 (1984) · Zbl 0985.68518
[41] 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
[42] 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) · Zbl 0578.68009
[43] Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM TOPLAS 4, 455–495 (1982) · Zbl 0483.68013
[44] 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
[45] Reinecke, R.: Networks of communicating processes: a functional implementation. Manuscript, Dept. Comput. Sci., Univ. of Kaiserslautern 1983
[46] Roscoe, A.W.: A mathematical theory of communicating processes. D. Phil., Thesis, Oxford Univ. 1982
[47] 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
[48] Smyth, M.B.: Power domains. J. Comput. Syst. Sci. 16, 23–26 (1978) · Zbl 0391.68011
[49] Soundararajan, N., Dahl, O.-J.: Partial correctness semantics of communicating sequential processes. Research Rep. No. 66, Inst. of Informatics, Univ. of Oslo 1982
[50] Stoy, J.E.: Denotational semantics: the Scott-Strachey approach to programming language theory. Cambridge: MIT Press 1977 · Zbl 0503.68059
[51] Winskel, G.: Events in computation. Ph. D. Thesis, Dept. Comput. Sci., Univ. of Edinburgh 1980
[52] 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) · Zbl 0566.68014
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.