Information Technology Reference
In-Depth Information
Definition 9.
Given a design (
θ
,
Λ)
, where
θ
= (V,
Γ
, tv, ta, D) and
Λ
is a triple (I, R,
L, U), a
model
of (
θ
,
Λ)
is an interpretation structure
S
=(
T
,
A
,
G
) for
θ
, such that:
•
(
S
,w
0
)
t
I
•
for every g
∈
Γ
, a
∈
D(g), e
∈
G
(g) , and (w, e, w')
∈
→
, then
A
(a)(w')=
[R(g,a)]
s
(w)
•
for every w
∈
W
and g
∈
Γ
, if e
∈
G
(g) and for some w'
∈
W
, (w, e, w')
∈
, then (
S
,w)
t
L(g).
That is to say, a
model
of a design is an interpretation structure for its signature that
enforces the assignments, only permits actions to occur when their enabling guards
are true, and for which the initial state satisfies the initialization constraint.
A model is said to be a
locus
if it is a locus as an interpretation structure, which en-
forces the encapsulation of local attributes.
This classification of models reflects the existence of different levels of semantics
for the same design (taken as a set of models), depending on which subset of the set
of its models is considered. These different semantics are associated with different
notions of superposition (design morphism) that have been used in the literature,
namely regulative, invasive and spectative. This means that there is no absolute no-
tion of semantics for designs: it is always relative to the use one makes of designs.
This corresponds to the categorical way of capturing the “meaning” of objects
through the relationships (morphisms) that can be defined between them.
→
1.3 The Morphisms Between Designs
The concept of superposition has been proposed and used as a structuring mechanism
for the design of parallel programs and distributed systems. Structure preserving
transformations are usually formalized in terms of morphisms between the objects
concerned, thus justifying the formalization of superposition in terms of morphisms of
designs in CommUnity.
Having defined designs over signatures in the above section, we first introduce
signature morphisms as a means of relating the “syntax” of two designs.
Definition 10.
A
signature morphism
σ
from a signature
θ
1
=(V
1
,
Γ
1
, tv
1
, ta
1
, D
1
) to
θ
2
=(V
2
,
Γ
2
, tv
2
, ta
2
, D
2
) consists of a total functions
σ
α
: V
1
→
V
2
, and a partial map-
ping
σ
γ
:
Γ
2
→
Γ
1
such that:
•
For every v
∈
V
1
,
σ
α
(v) has the same type as v.
•
For every o
∈
out(V
1
),
σ
α
(o)
∈
out(V
2
).
•
For every p
∈
prv(V
1
),
σ
α
(p)
∈
prv(V
2
).
•
For every i
∈
in(V
1
),
σ
α
(i)
∈
out(V
2
)
∪
in(V
2
).
For every g
∈
Γ
2
, such that
σ
γ
(g) is defined:
•
g
∈
sh(
Γ
2
), then
σ
γ
(g)
∈
sh(
Γ
1
).
•
g
∈
prv(
Γ
2
), then
σ
γ
(g)
∈
prv(
Γ
1
).
D
2
(g).
A signature morphism maps attributes of a design to attributes of the system of which
it is a component, and the direction of the mapping is reversed for actions. The first
•
σ
α
(D
1
(
σ
γ
(g))
⊆
Search WWH ::
Custom Search