Introduction

A model for reactive computation, for example that of labelled transition systems [Kel76], or a process algebra (such asACP [BW90], CCS [Mil89], CSP [Hoa85]) can be used to describe both implementations of processes and specifications of their expected behaviours. Process algebras and labelled transition systems therefore naturally support the so-called single-language approach to process theory, that is, the approach in which a single language is used to describe both actual processes and their specifications. An important ingredient of the theory of these languages and their associated semantic models is therefore a notion of behavioural equivalence or behavioural approximation between processes. One process description, say SYS, may describe an implementation, and another, say SPEC, may describe a specification of the expected behaviour. To say that SYS and SPEC are equivalent is taken to indicate that these two processes describe essentially the same behaviour, albeit possibly at different levels of abstraction or refinement. To say that, in some formal sense, SYS is an approximation of SPEC means roughly that every aspect of the behaviour of this process is allowed by the specification SPEC, and thus that nothing unexpected can happen in the behaviour of SYS. This approach to program verification is also sometimes called implementation verification or equivalence checking.

Designers using implementation verification to validate their (models of) reactive systems need only learn one language to describe both their systems and their specifications, and can benefit from the intrinsic compositionality of their descriptions, at least when they are using a process algebra for denoting the labelled transition systems in their models and an equivalence (or preorder) that is preserved by the operations in the algebra.