Design in CommUnity with Extension Morphisms - Formal Methods and Hybrid Real-Time Systems - page 448

we know that, in a well formed configuration diagram, all the components are inter-
connected by cables through regulative superposition morphisms, the component to
be replaced by the extended design is connected to a cable by the regulative superpo-
sition morphism, as shown in Figure 2. We will show that the regulative superposition
can be combined with the extension morphism to obtain a new regulative superposi-
tion from the cable to the extended component. This then allows us to apply the
mechanisms of CommUnity to obtain the semantics of the extended configuration
diagram, the colimit, which again consists of components connected through cables
and superposition morphisms. Again, it is crucial to have the notion of cables to inter-
connect the components, to ensure that the composition of regulative superposition
and extension morphism will give a new regulative superposition.

Fig. 2. Combining regulative superposition and extension morphisms

Proposition 8. Suppose m is a regulative superposition morphism from cable θ to

design C i and n is an extension morphism from design C i to design E i ; there exists a
regulative superposition morphism n' from cable m. θ to design E i such that n'=n •

Proof
The morphism n' is defined as follows:

• n' α is a total function: for every channel v in θ , n' α (v) = n α (m α (v)).

n' γ is a partial mapping: for every action g in E i , if n γ (g) is defined and m γ (n γ
(g)) is also defined, n' γ (g) = m γ (n γ (g)); otherwise, it is undefined.
Since an extension morphism is also a signature morphism, we know n' is a signature
morphism. To check if n' is a regulative superposition morphism, we need to check
the following conditions:
•

•

I Ei ⇒ n'(I θ ).
Because n is an extension morphism, there exists a formula α , using only channels

∨

contained in ( − n α (V Ci )), and α is satisfiable, t I Ei ⇔ n(I Ci ) ∧α . Ei

We have I Ei ⇒ n(I Ci ), I Ci ⇒ m(I θ ), so n(I Ci ) ⇒ n(m(I θ )) ⇔ n'(I θ ), and I Ei ⇒ n'(I θ ).

• If v ∈ loc( θ ), g ∈ Γ Ei and n' α (v) ∈ D Ei (g), then g is mapped to an action

n' γ (g) and v ∈ D θ (n' γ (g)).

• For every g ∈ Γ Ei where n' γ (g) is defined, if v ∈ loc( θ ) and g ∈ D Ei (n' α (v)),

then R Ei (g, n' α (v)) ⇔ n' α (R θ (n' γ (g),v)).

) is empty, so these two conditions hold. Because θ only contains input channels, loc( θ