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.
 
Search WWH ::




Custom Search