Hiding certain interactions - Abstraction by "projection"

If a system is composed of several components, one is often interested in viewing the system as a black box, showing only the external interactions, but not the interactions between the components within the system. One says that the internal interactions should be hidden. In other cases, one may be interested only in the interactions at one particular interface of the specified system, ignoring the interactions at another interface (called projection onto the visible interface).

Such a black-box view of a composed system or a projection on a subset of the interfaces is an abstraction of the original (more detailed) specification. The abstract view can be obtained from the original view:

An important example: Protocol verification

  1. The service specification defines the requirements that the system containing the protocol entities and the underlying medium should satisfy.
  2. The behavior of this system can be obtained by reachability analysis from the behavior of the two protocol entities and the medium.
  3. The service specification takes a more abstract view by ignoring (hiding) the interactions between the protocol entities and the medium (the exchange of protocol messages). Therefore, before the behavior of the protocol system can be compared with the specified behavior of the service, we should hide the medium interactions from the detailed view of the protocol system behavior.
  4. Then we obtain the abstract behavior of the protocol system which involves the same interactions as the service specification. We therefore can check whether these two specifications are equivalent, or whether at least all traces of the protocol system are included in the traces specified by the service (trace inclusion - to verify the safeness of the protocol).

Do this for a simple example, possibly using LTSA. See example CommProtocol-simple.lts (For the principle of safeness checking, see coffeeMachine - with tea safeness.lts )

See also the proof of the Alternating Bit Protocol (see my paper from 1978 - this is probably the first paper where it is shown how one can formally verify that a protocol specification gives rise to a given communication service)

Created: September 18, 2014