Wiley-Interscience, 2000. — 320 p.
This book supports advanced level courses on concurrency covering timed and untimed CSP. The first half introduces the language of CSP, the primary semantic models (traces, failures, divergences and infinite traces), and their use in the modeling, analysis and verification of concurrent systems. The second half of the book introduces time into the language, brings in the timed semantic model (timed failures) and finally presents the theory of timewise refinement which links the two halves together.