Information Technology Reference
In-Depth Information
System
=
df
|
[
var
x
1
:
T
1
,x
2
:
T
2
, out, inout
:
FR,
diff
1
, diff
2
:
NZP,
p1 running, p2 running, wr
:
Bool
• x
1
:= (0
,
0);
x
2
:= (0
,
0);
out
:= (0
,
0);
inout
:= (0
,
0);
wr
:=
false
p1 running
:=
false
;
p2 running
:=
false
alt
PUMP1 ON
:
g
1
→
p1 running
:=
true
;
inout
:= (0
..Max,
0)
PUMP1 OFF
:
g
2
→
p1 running
:=
false
;
inout
:= (0
,
0)
PUMP2 ON
:
g
3
→ p2 running
:=
true
;
out
:= (0
..Max,
0)
PUMP2 OFF
:
g
4
→ p2 running
:=
false
;
out
:= (0
,
0)
WATER REQ(X)
:
g
5
→ wr
:=
X
with
¬
(
g
1
∨ g
2
∨ g
3
∨ g
4
∨ g
5
):
add
(
diff
2
, out, inout
)
∧ add
(
diff
1
, inout, in
)
∧
d/dt
(
x
1
, diff
1
)
∧ d/dt
(
x
2
, diff
2
)
]
|
:
in
Fig. 6.
Qualitative action system of the two-tank system
Similarly,
g
1
and
g
2
can be given as follows:
g
1
=
df
x
2
< Reserve
∧
x
1
=
Full
∧¬
p1 running
x
2
=
Full
)
The first four controller actions are observable by a user of the system. The
fifth discrete action
WATER REQ(X)
is controllable and models a user scenario
where water is requested when tank
T
2 is full and the water is being turned off
as soon as the water level drops below the
Reserve
level. Guard
g
5
expresses this
behavior:
g
5
=
df
(
g
2
=
df
p1 running
∧
(
x
1
<Empty
∨
¬
∧
x
2
=
Ful l
∧
∨
∧
x
2
<
Reserve
∧
wr
X
=
true
)
(
wr
X
=
false
)
Since
WATER REQ(X)
is a controllable action, the tester sets the Boolean pa-
rameter
X
for requesting water or not depending on the described user scenario.
All discrete actions are combined via demonic choice.
The qualitative action in the
with
section consists of an
evolution guard (EG)
,
the :
arrow denoting a qualitative action, and a body comprising a set of QDEs.
If the EG holds in a certain state, the corresponding evolution consists of the
set of qualitative traces which terminate in post-states where EG does not hold
anymore. If there exist no post-states, the evolution does not terminate. The
weakest precondition (wp) semantics of qualitative actions is described in [2]
and can be interpreted as a non-deterministic update statement. The action
relates the initial state of a qualitative evolution to a set of post-states. From
these post-states further actions or evolutions can proceed. The wp semantics of
qualitative action systems ensures that only terminating actions are executed.