Towards an Algebra of Abstractions for Communicating Processes

It is often desirable to describe the interface of an implementation system at a different (usually more detailed) level of abstraction to the interface of the relevant specification. This calls for a relation aimed at formalising the notion that a process is an acceptable implementation of another target process in the event that they possess different interfaces. This paper formulates a suitable implementation relation between the observable behaviours of the implementation and the target process using CSP. Interface difference and bridging is modelled by endowing the implementation relation with parameters, called extraction patterns, instrumental to interpreting implementation behaviour as target behaviour. Reasonable notions of implementation and extraction patterns should result in a relation satisfying the realisability and compositionality properties. The former means that, if target and implementation in fact have the same interface, then the implementation relation between them collapses into the standard implementation pre-order of CSP. Compositionallty allows a target composed of several connected systems to be implemented by connecting their respective implementations. With respect to previous work, the paper drops a restriction that prevented broadcast and other group communication to be modelled, and admits fully general specification processes. The novelty of the approach presented here is that it introduces operations over extraction patterns, mimicking (and being compatible with) operations on processes.