Software Engineering with PSF

Implementation Techniques

It is only useful to invest a lot of effort in the specification of software systems at different levels of design if we can relate the specifications to eachother. We describe the techniques we use to get from an architecture specification to a ToolBus application specification. These techniques are important in our software engineering process as they compress a large number of algebraic law applications into a few steps and so make the process feasible.

Horizontal Implementation

Given two processes S and I, I is an implementation of S if I is more deterministic than (or equivalent to) S. As the actions S and I perform belong to the same alphabet, S and I belong to the same level of abstraction. Such an implementation relation is called horizontal.

To achieve a horizontal implementation we use parallel composition, which can be used to constrain a process. Consider process P = a . P, which can do action a at every moment. We put P in parallel with the process Q = x . b . Q, where x a is local action of Q, and we define the communication a | b = c. If we enforce the communication by encapsulation, process P can only do action a whenever process Q has first done action x. So process P is constrained by Q and P || Q is a horizontal implementation of P, provided Q only interacts with P through b. This form of controlling a process is also known as superimposition or superposition.

Vertical Implementation

We use action refinement as a technique for mapping abstract actions onto concrete processes. This is also called vertical implementation. With vertical implementation we want to relate processes that belong to different levels of abstraction, where the change of level usually comes with a change of alphabet. For such processes we like to develop vertical implementation relations that, given an abstract process S and a concrete process I, tell us if I is an implementation for the specification S. More specifically, we want to develop a mapping of abstract actions to sequences of one or more concrete actions so that S and I are vertical bisimilar.

We give a rationale of vertical implementation. Consider the processes P = a . b with a an internal action and Q = c . d . e with internal actions c and d. If we refine abstract action a from process P to the sequence of concrete actions c . d and rename action b to e we obtain process Q. The processes P and Q are vertical bisimilar with respect to the mapping consisting of the above refinement and renaming.

We can explain the notion vertical bisimilar by the following. We hide the internal action a of process P by replacing it with the silent step τ to obtain P = τ . b. Applying the algebraic law x . τ = x gives us P = τ . τ . b. If we now replace the first τ with c and the second with d, and rename b into e we obtain the process Q. With H as hide operator and R as renaming operator we can prove that

R{ b → e } ( H{ a } ( P ) )
H{ c,d } ( Q )
are rooted weak bisimilar (see the illustration below). So vertical bisimulation is built on rooted weak bisimulation as horizontal implementation relation.

Implementation relations