AN INTRODUCTION TO TIMED CSP

Abstract

Timed CSP is an extension of Communicating Sequential Processes which includes timing information. It can be used to model timedependent 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 esp, aimed at those familiar with Hoare's book on esp, [H85]. 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.