Information Technology Reference
In-Depth Information
both tanks empty, both pumps turned off, and some non-zero inflow rate into
tank T 1. The two keywords alt and with are used to denote the principle of
hybrid alternation: the discrete actions in the alt block are alternated with the
continuous action in the with block. In order to model reactive behavior, we give
the controller priority over the environment. In other words, whenever an action
of the alt block (which models the controller) is enabled for execution, a possibly
running continuous action terminates and the action of the alt block is executed.
This type of alternation is called interrupting prioritized alternation .Noticethat
the controller eventually has to reach a stable state in its computation where
it waits for environmental updates. Otherwise, the environment and hence the
progress of time would be blocked. The work in [15] discusses various kinds of
hybrid alternation.
In order to apply standard LTS-based testing techniques we label each action
with a name, denoting an event. For environmental changes (the execution of
qualitative actions) we introduce the so-called qual event which may have pa-
rameters. The parameters determine the valuation of certain model quantities at
the end of an evolution. This event view provides a further level of abstraction
since, for blackbox testing, we are only interested in the external event behavior
of a system. If the tester is only interested in the discrete controller events, the
environmental qual events can also be hidden and considered as internal. Even
in this case, a wrong environmental behavior can be detected if it has influence
on the discrete controller events. Internal events are denoted with τ .
By executing a (qualitative) action system we obtain the set of all possible
event sequences starting from the initial state. This gives us the trace (LTS)
semantics of the action system. The trace semantics of qualitative action systems
is described in [6]. Hence, our test model is an LTS obtained by exploration rather
than the action system itself.
We need to create five discrete actions in order to model the controller. Each
discrete action has a name (label) followed by a guard and an action body. When
the action guard holds in a certain computation state, the body is executed
and the model variables are updated accordingly. For instance, the first discrete
action
PUMP1 ON : g 1
p1 running := true ; inout := (0 ..M ax, 0)
has some guard g 1 and switches on pump P 1 by setting the Boolean variable
p1 running to true and the pump to some non-zero, steady flow rate. The action
system in Figure 6 still has general guards g 1 to g 5 instead of concrete ones.
Hence, we need to find the correct guards so that our controller behavior matches
the requirements. Starting with the first requirement that specifies when P2
should be enabled we can replace g 3 by:
g 3 = df wr
∧¬
p2 running
x 2 > Empty
Requirements 2 and 3, dealing with cases when to stop P2, can be translated
into guard g 4 :
g 4 = df p2 running
(
¬
wr
x 2
Empty )
Search WWH ::




Custom Search