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

4.3 A System Development Meta Model, Development Relations: Refinement

The system meta model describes the building blocks of all system models. During
system development, several system models are constructed that - in an ideal case -
are formally related by refinement relations.
We are not only interested in the system modeling elements, the system views, and
how they fit together to a complete system description. We are also interested in
relating the models as they are successively constructed in the development process.
For this purpose we introduce refinement relations between models. We work with
three levels of refinement:
• Horizontal refinement also called property refinement ; by property refinement we

add properties that restrict the behavior of the system and thus make a system
more deterministic.

• Vertical refinement also called design or implementation ; by a design or

implementation step we replace an interface by a design. A design is given by a
decomposition of a system into subsystems or a state machine.

• Granularity refinement also called interaction refinement - levels of abstractions ;

by a refinement step changing the level of abstraction we replace system models
by a more concrete ones, for instance, by systems with finer grained actions, state
transitions, or messages.
These refinements are mathematically relations between modeling elements. These
relations form partial orderings. We assume that vertical refinements are special cases
of horizontal refinement, which is in turn a special case of granularity refinement.

4.3.1 Property Refinement
During development we develop systems step by step adding more and more detail.
We work with a refinement relation to relate models to those with more specific
properties. Therefore we speak of property refinement or semantic compatibility . This
relation can be introduced for all described system views:

IB
If M ≈> M' holds we say M refines to M' or M is refined by M'. Moreover we
assume that refinement implies syntactic compatibility
A ≈> B ⇒ A >> B
Each refinement relation is assumed to be a partial ordering. Of course this form of
refinement should be compatible with the introduced notions of composition and
abstraction.

≈> : HCS × HCS →

α IF (M') compatibility of refinement
In mathematical terms, abstraction is monotonic for refinement (for X

M ≈> M' ⇒ α IF (M) ≈> IF

∈ {IF, SM,

PRC } ) .

N' compositionality of refinement
In mathematical terms, composition is monotonic for refinement. By refinement
we can relate models and parts of models.

M ≈> M' ∧ N ≈> N' ⇒ M ⊗ N ≈> M' ⊗

4.3.2 Implementation as Refinement
Complex systems are modeled during development at different levels of abstraction
and granularity. We work with a refinement relation to relate models at different