Software Design


We introduce explicit levels of abstraction in the FBS framework (R-FBS) by considering the design of two models, M and M', for a particular system. The model M' is supposed to be a faithful implementation of the model M. Both models have their own design process, FBS and FBS', each of which can be described by the function-behaviour-structure framework.

The two design processes can be integrated, so that the processes that play a role in the refinement, evalution of the refinement, and reformulation of the refinement become clear. The figure below shows the integration of the two design processes.

Refinement in the FBS framework

Below we describe the changes in processes because of this integration.


Each element of FBS' can be considered a refinement of the associated element of FBS. In the following we describe how the refinement processes between the two frameworks take place.
Functionality refinement ({D, F} → F')
As the structure S consists of the components and their interaction for model M, the description D describes the functionality of these components and the interactions. It is this functionality together with functionality F that makes up the functionality F' for model M'. This refinement of functionality is indicated by 1 in the figure.
Expected behaviour refinement ({Be, F'} → Be')
The expected behaviour Be' can be obtained by refining the expected behaviour Be with refinements extracted from F'. This is indicated by 2 in the figure.
Structure refinement ({S, Be'} → S')
In a FBS framework the structure is synthesized from the expected behaviour of the model. We cannot obtain the structure S' from Be' in this way, since S' must be a refinement of S. We have to synthesize S' from S and use refinements that are based on Be'. This is indicated by 3 in the figure.
Documentation refinement ({D, S'} → D')
The description D' is the addition of the description D and the description of the refinement processes. This is indicated by 4 in the figure.

Behaviour Evaluation

Besides the behaviour evalution on both levels, we have to check if M' is a true implementation of M.
Behaviour evaluation (Bs ↔ Bs')
We can do this by comparing a refined Bs with Bs'. But that leaves us with the problem how to refine Bs. We can however do the reverse. Instead of refining Bs we can abstract Bs' and compare it with Bs. If the behaviours do not match, the refinement process is wrong and has to be adjusted. The adjustment can be done through reformulation processes described in the next section.


The design frameworks for the models M and M' contain reformulation processes. For the model M these are the standard processes described earlier, but for the model M' the reformulations have to be such that the elements stay within the refinements of their corresponding abstract elements.

Function reformulation (F' → F)
Behaviour reformulation (Be' → Be)
Structure reformulation (S' → S)
The situation can occur that a reformulation of one of the elements for model M' is necessary and that because of this reformulation it no longer conforms with the corresponding abstract element for model M. In that case, the current design must be rejected and a reformulation of the corresponding element for model M have to take place.