Information Technology Reference
In-Depth Information
Proposition 5.
Let
σ
be an extension morphism from a design (
θ
1
,
Λ
1
)
to another
design (
θ
2
,
Λ
2
)
. Then, every model of (
θ
1
,
Λ
1
)
can be expanded to a corresponding
model of (
θ
2
,
Λ
)
.
2
The rationale behind the definition of extension morphisms is the characterization of
the substitutability principle (a property that can be shown to fail for invasive super-
position, a more general and less predictable way of breaking encapsulation, as de-
fined in [15]). The above result shows that, if there exists an extension morphism
σ
between two designs (
θ
1
,
Λ
)
and (
θ
2
,
Λ
)
(and this extension is realisable), then all
1
2
behaviours exhibited by (
. Since superposition
morphisms, used as a representation of “clientship” (strictly, the existence of a super-
position morphism between two designs indicates that the first is part of the second,
as a component is part of a system when the first is used by the system), restrict the
behaviours of superposed components, it is guaranteed that all behaviours exhibited
by a component when this becomes part of a system will also be exhibited by an ex-
tension of this component, if replaced by the first one in the system. Of course, one
can also obtain
more behaviours
, and this is the intention behind the definition of
extension morphisms, resulting from the explicit use of new actions of the compo-
nent. But if none of the new actions are used, then the extended component behaves
exactly as the original one did.
Now we introduce the relationship of refinement between two components, which
we need to enable us to use the architectural concept of connector.
θ
1
,
Λ
)
are also exhibited by (
θ
2
,
Λ
)
1
2
Definition 15.
A
refinement morphism
σ
from a design (
θ
1
,
Λ
1
)
to another design (
θ
2
,
Λ
2
)
is a signature morphism
σ
:
θ
1
→
θ
2
such that:
1
For every i
∈
in(V
1
),
σ
α
(i)
∈
in(V
2
).
2
σ
α
is injective on input and output channels.
3
σ
γ
is surjective on shared actions in
Γ
1
.
4
t
(I
2
⇒
σ
(I
1
)).
5
If v
∈
loc(V
1
), g
∈
Γ
2
and
σ
α
(v)
∈
D
2
(g), then g
is mapped to an action
σ
γ
(g) and v
∈
D
1
(
σ
γ
(g)).
For every g
∈
Γ
2
where
σ
γ
(g) is defined,
6
If v
∈
loc(V
1
) and g
∈
D
2
(
σ
α
(v)), then
t
(R
2
(g,
σ
α
(v)) ⇒
σ
α
(R
1
(
σ
γ
(g), v))).
7
t
(L
2
(g) ⇒
σ
(L
1
(
σ
γ
(g)))).
For every shared action g
∈
Γ
1
,
∧
σ
γ
-1
(g))).
8
t
(
σ
(U
1
(g)) ⇒
U
2
(
A refinement morphism identifies a way in which design (
θ
1
,
Λ
1
)
is refined by a more
concrete design (
. The first three conditions must be established to ensure that
refinement does not change the interface between the system and its environment.
Notice that we do not require
θ
2
,
Λ
2
)
σ
γ
to be injective because the set of actions in the target
design that are mapped to action g of the source design can be viewed as a menu of
Search WWH ::
Custom Search