Affiliations: School of Computing Science, University of Newcastle,
Newcastle upon Tyne NE1 7RU, UK | Dipartimento di Matematica e Informatica
Università di Catania, I-95125 Catania, Italy
Abstract: We present here an implementation relation intended to formalise the
notion that a system built of communicating processes is an acceptable
implementation of another base, or target, system in the event that the two
systems have different interfaces. Such a treatment has clear applicability in
the software development process, where (the interface of) an implementation
component may be expressed at a different level of abstraction to (the
interface of) the relevant specification component. Technically, processes are
formalised using Hoare's CSP language, with its standard failures-divergences
model. The implementation relation is formulated in terms of failures and
divergences of the implementation and target processes. Interface difference is
modelled by endowing the implementation relation with parameters called
extraction patterns. These are intended to interpret implementation behaviour
as target behaviour, and suitably constrain the former in connection to
well-formedness and deadlock properties. We extend the results of our previous
work and replace implementation relations previously presented by a single,
improved scheme. We also remove all the restrictions previously placed upon
target processes. Two basic kinds of results are obtained: realisability and
compositionality. The latter means that a target composed of several connected
systems may be implemented by connecting their respective implementations. The
former means that, if target and implementation in fact have the same
interface, then the implementation relation they should satisfy collapses into
standard implementation pre-order. We also show how to represent processes and
extraction patterns in a manner amenable to computer implementation, and detail
a graph-theoretic restatement of the conditions defining the implementation
relation, from which algorithms for their automatic verification are easily
derived.
Keywords: theory of parallel and distributed computation, behaviour abstraction, refinement, communicating sequential processes, compositionality, verification,
