In this paper we describe the calculus TCCS, an extension of the process algebra CCS with temporal constructs. The calculus is useful for the formal analysis of the timing aspects of systems, as well as their functional behaviour. Such aspects include when events can and must occur, as well as how fast a process may execute. The paper includes extensive examples, as well as a detailed description of the theoretical underpinnings of the language. We also include a description of a logic for specification, which is an extension of Hennessy-Milner logic. Finally, we present a brief comparison with various other similar approaches to the analysis of the temporal properties of systems. Contents
Faron Moller, Chris M. N. Tofts