Programming Research Group Technical Monograph PRG-112

Janet E Barnes

DPhil thesis Hilary 1993, 193 pages, ISBN 0-902928-89-9

A mathematical theory of synchronous communication is presented. The process algebra SCSP, shares many of its constructors with Hoare's Communicating Sequential Processes. It models components of a distributed system as processes evolving in lockstep. A synchronous variant, SRPT, of Josephs' Receptive Process Theory, which distinguishes between input and output events in its model of communication, is also investigated.

The language SCSP is given a denotational semantics. The semantic model captures the behaviour of processes using failures-divergences information. SCSP exhibits sufficient algebraic laws to form a sound and complete proof system with respect to the semantics. This allows reasoning about concurrent systems by means of algebraic manipulation of process expressions. The notation is extended to capture communication of data via channels and is used to specify a token ring protocol. SCSP is sufficiently expressive to establish temporal details of the protocol.

SRPT can be interpreted as a receptive sublanguage of SCSP. This is demonstrated by embedding both the language and its semantic model in those of SCSP. The embedding allows many of the mathematical results concerning SRPT to be deduced from their counterparts in SCSP. SRPT is shown to be applicable to the modelling of synchronous circuits. The notion of discrete time in the algebra captures the clock's behaviour while the receptive nature of SRPT matches the communication of signals in a circuit. By introducing a notion of timewise abstraction, the effect of variation in the speed at which circuits are clocked can be analysed. Timewise abstraction is also applied to the analysis of pipes.