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

space is the choice of a set of typed attributes such that each valuation of this
attributes defines a state.
Given initial states ) defines a system in terms of a

state machine. By SM we denote the set of all state machines.

Λ ⊆ State and the pair ( Δ , Λ

4.2.3 Abstraction: The Interface Model
In general, state machines provide a rather detailed model of a system. Often we are
interested in more abstract views. In particular, from a user's point of view we are
often not interested in the concrete states of a system. For state machines with input
and output or with labeled transitions the abstraction is quite obvious. If the labels
describe the effects of the machine to the outside world we are only interested in the
labels but not in the states.
For unlabeled state transition systems we may divide the states into local and
nonlocal parts. In the cases of state spaces defined by attributes we speak of local and
nonlocal attributes. We may furthermore distinguish between attributes that can only
be read or written by the machine and those that can only be read or written by the
environment.
To begin with, we introduce abstractions between state machines. Mathematically,
an abstraction is a mapping of the form

SM
This is only a syntactic notion so far. Not every mapping between state machines is
to be called an abstraction. Particular behavioral similarities are required that we will
discuss in detail later. In fact, there are, in general, many abstraction mappings
between state machines.
To begin with we are interested in syntactic interfaces . A syntactic interface
describes syntactic properties of a system that determine if it can be composed with
another system (since they syntactically fit together) or if a system A can be replaced
another one B in any context without running in any syntactic difficulties. Then B is
called syntactically compatible for A and we write A >> B. We assume that the
syntactic compatibility relation >> is partial preorder. If A >> B and A >> B then we
write A ≈ B and say that A and B are mutually syntactically compatible .
In the interface model we abstract from all details in the state machine model that
are not relevant for working with a system. An interface view provides therefore an
abstraction. By IF we denote the set of all interfaces. We assume that there is a
canonical abstraction function called interface abstraction :

α SM / SM : SM →

α SM / IF : SM → IF interface abstraction

We require for all we interface behaviors F ∈ IF

F ≈ α SM / IF (F))
The abstraction function maps a state machine onto its interface. The interface is
also called black box view or observable behavior . In fact, we also define abstractions
between interfaces:

IF
We require for all we interface behaviors F

α IF / IF : IF →

∈ IF