Denotational semantics of communicating sequential programs

Theory of operating systems (68N25) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The language CSP (Communicating Sequential Programs) of Hoare is an elegant notation for the description of communicating systems. A denotational semantics of CSP is given based on a mathematical functional model of communicating processes by functions mapping for every initial state an input stream, i.e. a finite or infinite sequence, of offers onto a set of output streams of reactions plus a final state which is defined only if the program terminates properly. An offer is either the request for sending the value of a variable or the offer to send the value of a variable. A reaction is either the value of a variable requested or the acknowledgement for a value offered or a reject signal. The reject signal is only given as output if an offer cannot be accepted. This gives a very general view of communicating processes as stimulus/response systems. The main purpose of this definition is found in serving as a reference for specification and verification methods.

Recommendations

Cites work

Cited in

(20)

This page was built for publication: Denotational semantics of communicating sequential programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1088402)