Information Technology Reference
In-Depth Information
For a more detailed description of the process of qualitative behavior inference
and the possible qualitative constraints see [13]. The following section presents
the hybrid model of our running example.
4 System Modeling with Qualitative Action Systems
In the previous section, we have developed a set of QDEs expressing the con-
tinuous evolutions of our running example. For our hybrid system model to be
complete, we now have to merge the qualitative evolutions of the environment
with the behavior of the controller into a single qualitative action system model.
Qualitative action systems are based on the formalism of action systems by Back
et al. [5] that provide a framework for describing discrete and distributed sys-
tems. The actions are statements in the form of Dijkstra's guarded commands
where the semantics is defined via weakest precondition predicate transformers.
An action system (see Equation 3) consists of a block of variable declarations
followed by an initialization action
S
0
assigning to each variable an initial value
and a
do od
block looping over the non-deterministic choice of all actions. Vari-
ables declared with a star are exported by an action system and can be imported
by others in the import list
I
at the end of the action system block. Exported
variables have to be unique among all other exported variables.
AS
=
df
|
[
var
Y
:
T
•
S
0
;
do
A
1
...
A
n
od
]
|
:
I
(3)
In order to specify distributed concurrent systems, several action systems can be
composed in parallel. For two action systems
A
1
and
A
2
the import list of the
resulting system gets (
u
1
∪
v
2
)where
u
1
,u
2
are the imported variables
and
v
1
,v
2
are the exported variables of
A
1
and
A
2
respectively. It follows that
communication of parallel running action systems is modeled by access to shared
(imported/exported) variables which is a good choice (easy semantics) when
modeling distributed and parallel systems.
In order to model our water-tank system as action system, we have to be more
precise on its requirements:
u
2
)
\
(
v
1
∪
1. If a button
WaterRequest
is pressed (on) and provided
T
2isnot
empty (water level above
Reserve
), start pump P2 and pump water
out of tank
T
2.
2. If P2 is running and
WaterRequest
is not pressed, stop P2.
3. If P2 is running and the water level of
T
2dropsto
Empty
,stopP2.
4. If tank
T
2 gets empty (water level below
Reserve
mark) and
T
1is
full, pump water out of tank
T
1intotank
T
2bystartingpumpP1.
5. If pump P1 is running and the water level in tank
T
1dropsto
Empty
,
then stop P1.
6. If pump P1 is running and the water level in tank
T
2 reaches
Full
,
then stop P1.
The formal model of the system is given in Figure 6 and comprises three sections.
In the
var
section all variables are declared and initialized: the system starts with
