Programming Research Group Technical Monograph PRG-75

Jim Davies and Steve Schneider

August 1989, 70 pages, ISBN 0-902928-57-0

Timed CSP is an extension of Communicating Sequential Processes which includes timing information. It can be used to model time-dependent properties of concurrent systems. An algebraic notation is employed in the definition of processes, capturing the behaviour of a system in a clear and intuitive manner. A uniform hierarchy of semantic models for this notation is presented in [Re88]. Each semantic model identifies a process with a set of possible behaviours: by reasoning about these sets, we may establish properties of the corresponding processes.

This monograph contains two papers on Timed CSP. The first of these introduces the language of Timed CSP, aimed at those familiar with Hoare's book on CSP. The second presents a complete proof system for reasoning about the most useful class of Timed CSP specifications: behavioural specifications on timed failures. Together, these two papers provide a foundation for the specification and design of real-time concurrent systems using Timed CSP.