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

refinements that is made available for implementing g. Different choices can be made
at different states to take advantage of the structures available at the more concrete
level.
As for the “old actions”, the last two conditions in the refinement morphism defini-
tion require that the interval defined by their enabling and progress conditions must be
preserved or reduced. This is intuitive because refinement should reduce underspeci-
fication, so the enabling condition of any implementation must lie in the “old inter-
val”: the lower bound cannot be weakened and the upper bound cannot be strength-
ened. This is also the reason why the underspecification regarding the effects of the
actions of the more abstract design are intended to be reduced.

Proposition 6. The structure composed of CommUnity designs and superposi-
tion/refinement/extension morphisms constitutes a category SUP/REF/EXT, respec-
tively, where the composition of two morphisms σ 2 is defined in terms of the

composition of the corresponding channel and action mappings of

σ 1 and

σ 2 .
So, we can build superpositions/refinements/extensions incrementally. Most im-
portantly, SUP has finite colimits, i.e., we can compute the system corresponding to a
configuration of CommUnity designs whose channels and actions are synchronized
via cables and superposition morphisms. So called higher order connectors [29] are
defined in CommUnity to enable designers to use complex connectors between com-
ponents, in the style of software architecture approaches. These higher order connec-
tors are just CommUnity designs in which some components play a designated role ,
namely stating minimum requirements of actual components to be connected by the
connector in question. One can instantiate a role with a 'real' component by defining
a refinement from the role to the component. Thus, when designing a system using
components and connectors, we may end up with a configuration in which we see
both regulative superpositions and refinements. In order to calculate the intended
system form this configuration, we must eliminate the refinements and thus get a
configuration in SUP.
Luckily, we have the following crucial result about the joint use of refinement and
superposition morphisms. If we restrict the kinds of components used to interconnect
components to so called cables , we can combine superposition morphisms from such
a cable with a refinement. A cable is a design containing only input channels and its
actions having the following form g: true -> skip . We only expect input
channels in the cable, which can be used to interconnect designs, because output
channels cannot be used to connect the input channel of one design with the output
channel of another design, and it will make no sense to interconnect output channels
of different designs. Also we set the enabling guard and progress guard of each ac-
tion in the cable to true and set R(g) to skip (by skip we mean this action has no
effects on the local channels of the design), which is good enough to synchronize the
actions.

σ 1 and

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

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