Behaviour Abstraction for Communicating Sequential Processes

We investigate the notion that a system is an acceptable implementation of another base or target system, in the case that the two systems (or processes) have different interfaces. For instance, the base processes can be thought of as specifications, or ideal processes operating in an error-free environment, while the implementations model their actual realisations, operating in an error-prone environment and possibly employing a variety of fault-tolerant techniques. Using the CSP model, we relate implementations and base systems in terms of their observable behaviours. We obtain two fundamental results, viz. realisability and compositionality. The former ensures that implementations may be put to good use, while the latter guarantees that a target composed of several connected subsystems may be implemented by connecting their respective implementations.