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

Often we require additional syntactic properties for the components of a composed
system that assure, in particular, that the composition of the components is well
defined. The set of all composed system models with subsystems modeled by
interfaces is denoted by CS IF .
Similar mappings defining composed systems of components modeled by
processes or state machines are easily defined by the following functions.

ν PRC : IK → PRC

SM
This way we get systems structured into components modeled by processes or state
machines respectively. The sets of such composed system models with components
modeled by processes or state machines are denoted by CS PRC and CS SM respectively.
Due to the generalization of composition to we can consider architectures of the form

ν SM : IK →

PRC
where the components of an architecture are represented by interfaces, state machines
or processes.

ν : IK → SM ∪ IF ∪

4.2.7 System Hierarchies
So far we have only introduced concepts of flat, composed system models. Now we
define inductively the set of hierarchical composed systems. Let HCS denote the set of
all composed hierarchical systems . We define this set inductively by:
(0)

HCS 0 = SM ∪ IF ∪ PRC

(1) every function ν: IK → HCS n is in HCS n+1

We define

HCS n
This allows us to define hierarchical (and by a more sophisticated construction -
using ideas from domain theory - even recursive) systems. In most cases and also for
our purpose, however, finite hierarchies are sufficient. We define in full generality
that a hierarchical system is a mapping:

HCS = ∪

HCS
By the notion of component identifiers and hierarchical composed systems we
introduce a new concept into our system model namely that of an instance . In
particular, we include composed systems where one interface or one state machine is
used several times by assigning it to different component identifiers.

ν: IK →

4.2.8 The Use Relation in a System Hierarchy
In a large composed system we have generally many different constituents and
components. Typically there is a kind of hierarchy in a system model expressed by the
use-relation. We define functions such as

is_used DM / IF : DM × IF → IB

is_used IF / HCS : IF × HCS → IB

is_part IF / HCS : IF × HCS → IB