From “Formal Methods” to System Modeling - Formal Methods and Hybrid Real-Time Systems - page 33

Given the canonical function ρ IF / SM we define a canonical

PRC
such that for all we interface behaviors f

ρ IF / PRC : IF →

∈ IF define

ρ IF / SM (f))
This is, however, only one option to relate a canonical process to each interface.

ρ IF / PRC (f) = α SM / PRC (

4.2.5 Composed Systems: Composition
If we compose systems into larger ones out of given components we need an
operation of composition. In principle, compositions are useful for all the views and
models of systems described so far. To begin with we simply assume a binary
composition operator for each system view.

⊗ IF : IF × IF → IF

⊗ PRC : PRC × PRC → PRC

⊗ SM : SM × SM → SM

is commutative and associative. It may be a partial function, however.
Only certain components can be composed meaningfully. For each of these operators
we require:
A 1 >> B 1

Ideally ⊗

B 2 monotonicity of syntactic compatibility
We furthermore expect that interface abstraction distributes over composition:

∧ A 2 >> B 2 ⇒ A 1 ⊗ A 2 >> B 1 ⊗

⊗ SM M') compositionality
The same equation can be formulated for the process view. Due to the abstraction
function we easily may compose infaces f with state machines M by:

α SM/IF (M) ⊗ IF α SM/IF (M') = α SM/IF (M

α SM/IF (M) ⊗ IF f

or by

ρ IF/SM (f)
It is easy to show due to compositionality that the abstraction of the later is
identical to the first:

M ⊗ SM

ρ IF/SM (f))
We require, in addition, that the refinement relation that we introduce later is
compositional.

α SM/IF (M) ⊗ IF f = α SM/IF (M ⊗ SM

4.2.6 Composed Systems: Architecture
Assuming associativity and commutativity composition is easily generalized from
pairs of systems to sets and families of systems. Then we work with the notion of
component identifiers. A component is a system itself also called subsystem. Let IK
be a set of component identifiers. Then a composed system with components modeled
by their interfaces is defined by a mapping

IF
that associates an interface with each component identifiers. We speak of system
architectures .

ν IF : IK →