Information Technology Reference
In-Depth Information
%&
!
"#
$
'!(
Fig. 2.
Overview of our approach: Based on two QAS (a model of the SUT and a
mutated system model), we calculate the synchronous product modulo ioco on-the-fly,
i.e., we explore both QAS to gain the LTS semantics, add quiescence where needed,
and determinize the resulting LTS in parallel. Finally, we extract a controllable test
case from the synchronous product.
generator that combines a qualitative reasoning engine with an equivalence (con-
formance) checker. Note that we rely on classical notions of conformance defined
over labeled transition systems (LTS). This is achieved by interpreting an action
system as an LTS via a labeling of actions. We distinguish between input, output
and internal labels representing the communication events between tester and
SUT.
Figure 2 gives an overview of our test case generation approach. It relies on
two inputs: (a) a model of the SUT in the form of a QAS and (b) a mutated sys-
tem model, which is derived from the original QAS by applying a certain fault
model. Note that modeling (cf. Step 1) as well as fault injection (cf. Step 2)
have to be carried out manually. By the exploration of qualitative action sys-
tems, we are able to give them an LTS semantics. Our testing approach relies
on the well-known input-output conformance relation
ioco
[17]. For test case
generation, we check if the mutated model conforms to the original one. If not,
a counter-example is turned into a test case. The conformance check is imple-
mented as an on-the-fly calculation of the synchronous product modulo ioco of
the two given QAS, i.e., we explore both QAS to gain the LTS semantics, add
ioco's additional quiescence observation where needed (see Section 5.2), and de-
terminize the resulting LTS in parallel (cf. Step 3). In this way, only parts of
the QAS which are relevant for the test case generation are explored. Finally,
we extract a controllable test case, which is an LTS again.
In the rest of this paper we present the details of this approach. Section 2 in-
troduces our running hybrid systems example. Section 3 presents the qualitative
abstraction of continuous functions and Section 4 describes the modeling of a
hybrid system by means of QAS. Then, we discuss how test cases are identified
