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

think about a problem, a system, a product, or a process. In essence, it provides an
abstraction like any model. To find a good thought model is perhaps the most critical
modeling task since the thought model determines the adequacy of the future
development approach.
To make a thought model useful we have to find ways to precisely document,
communicate the model and to use it in analysis and design. A promising way to do
this is to represent a model in terms of well known, well understood concepts and
theories. Mathematics and logics is a good choice for that.
A mathematical model of a system or some of its aspects is a mathematical
structure, in general, an algebra, consisting of sets, functions, graphs, relations, and/or
logical predicates. It represents a thought model in mathematical terms. A good
mathematical model shows a number of properties such as modularity, flexibility and
thus fulfils a number of essential logical and mathematical properties. We come back
to this later. A mathematical model is an idealized abstraction that needs syntax to
represent it directly. We need techniques to write down, to document, and to
communicate mathematical and thought models.
Formalization of models in terms of mathematics and logics is not good per se.
However, if we are interested to reason about models in terms of well understood and
well established techniques formalization is a promising way to go. In principle,
formalization can be done by representing models in classical notation of mathematics
and logics. However, for an engineer it might be quite difficult and too demanding to
work out a mathematical model from scratch. Using standardized syntax and
modeling concepts for the description of models can help.
A description technique is a set of syntactic concepts (text, formula, graphs, or
tables) for the description of a thought model. Mathematical models provide the
semantic theory for description techniques. In essence, we use description techniques
(syntax) to represent a mathematical model (semantic) that formalizes the thought
model (abstraction and intention) for a particular development aspect. In the
following, we are at the same time interested in thought modeling, in mathematical
models and description techniques.
2.2 Description Techniques, Their Structures and Views
From what we have said about modeling it is obvious that model description
techniques are more useful if they address typical modeling needs and patterns, if they
provide support for reasoning about models, and if they support the purpose for which
the model was selected. If models are deployed in an engineering process for the
development, they have to support classical principles such as “divide an conquer”,
“levels of abstraction”, “separation of concerns”, “modularity” etc.
The description techniques and also the described models should therefore be
modular to support the modular decomposition and composition in the design of
systems and their description. This requirement induces a requirement on the
system model: there we need composition operators to construct such modular
systems. In addition, we are interested in an abstraction concept. Given a
description of a system building block, we look for an abstraction function that