Information Technology Reference
In-Depth Information
attributes” from being changed by “new actions”, i.e., actions of the target design not
mapped to the source design.
Now we will introduce the notion of extension morphism, related to ideas of
model-expansiveness. The motivation for extension morphisms originated from the
substitutability principle from object oriented program design, which says if a com-
ponent P
2
extends another component P
1
, then we can replace P
1
by P
2
and the “cli-
ents” of P
1
must not perceive the difference. This principle cannot be characterized by
regulative superpositions or refinement morphisms, as we may want to extend the
component by breaking encapsulation. This controlled breaking of encapsulation is
necessary when dealing with many aspects.
Definition 14.
An
extension morphism
σ
from a design (
θ
1
,
Λ
1
)
to another design (
θ
2
,
Λ
)
is a signature morphism
σ
such that:
2
1
σ
γ
is surjective.
2
σ
α
is injective.
3
There exists a formula
β
, which contains only channels from (V
2
−
σ
α
(V
1
)),
such that
β
is satisfiable and
t
I
2
⇔
σ
(I
1
)
∧
β
.
For every g
∈
Γ
2
for which
σ
γ
(g) is defined,
4
If v
∈
loc(V
1
) and g
∈
D
2
(
σ
α
(v)), then there exists a formula
β
, which con-
tains only primed channels from (V
2
'
−
σ
α
(V
1
)'), and
β
is satisfiable and
such that
t
σ
(L
1
(
σ
γ
(g))) ⇒ (R
2
(g,
σ
α
(v))
⇔
σ
α
(R
1
(
σ
γ
(g), v))
∧
β
).
5
If v
∈
loc(V
1
), g
∈
D
2
(
σ
α
(v)), then v
∈
D
1
(
σ
γ
(g)).
6
t
(
σ
(L
1
(
σ
γ
(g))) ⇒ L
2
(g)).
7
t
(
σ
(U
1
(
σ
γ
(g))) ⇒ U
2
(g)).
This definition of extension morphism was first given [8]. Because we expect that the
extended design can replace the original design in a system and the clients of the
original component should not perceive any difference, the first two conditions ensure
the preservation of its interface. The initialization condition of the original design can
be strengthened in its extended version, while respecting the initialization of the
channels of the original component, as required in the third condition. The fourth
condition indicates that the actions corresponding to those of the original design
should preserve the assignments to old channels and the assignments to new channels
must be realisable, when the safety guards of their image actions in the original design
are satisfied. The fifth condition establishes that for each action of the extended de-
sign that is mapped to an action of the original design, it can only modify old channels
that have been modified by the corresponding action of the original design. The last
two conditions indicate that both the enabling and progress guards can be weakened,
but not strengthened.
Because an extension morphism relaxes the enabling guard of the source design,
the reduct of a model of the target design may not be a model of the source design.
However, the model-expansive property holds for extension morphism [8], which
means the extended design can replace the source design and the clients of the origi-
nal design will not perceive the difference.
Search WWH ::
Custom Search