Specification-oriented semantics for communicating processes (Q1060838): Difference between revisions

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.