Information Technology Reference
In-Depth Information
The qualitative differential equation in (2) is totally defined, which means that
we could use predicate
true
as evolution guard. However, since the evolution is
considered atomic, it would never terminate and as a result the controller would
not be able to interrupt it once it is run. So in order to realize the interrupted
prioritized alternation between discrete and qualitative actions, we conjoin the
negated guards of all discrete actions to strengthen the evolution guard. This
guarantees that whenever the controller has something to do, it can interrupt
the evolution of the environment.
The imported variable
in
denotes that the inflow rate into the lower tank
is external to the system. In our example we assume a steady, non-zero inflow
rate, i.e.,
in
=(0
..M ax,
0). This concludes the description of the model and we
proceed with the testing techniques applied to our running example.
5 Model-Based Mutation Testing
Given the hybrid system model of the previous section, we derive test cases by
mutation: we compare the behavior of the original model with mutated ones
and extract behavior traces (tests) that allow us to distinguish implementations
conforming to the original specification from implementations that do not.
5.1 Mutation Testing
Classical mutation testing is a way of assessing and improving a test suite by
checking if its test cases can detect a number of injected faults in a program.
The faults are introduced by syntactically changing the source code following
patterns of typical programming errors. These deviations in the code are called
mutations. The resulting faulty versions of the program are called mutants. Usu-
ally, each mutant includes only one mutation. Examples of typical mutations
include renaming of variables, replacement of operators, e.g., an assignment for
an equivalence operator, and slightly changing Boolean and arithmetic expres-
sions. The number and kind of mutations depend on the programming language
and are defined as so called mutation operators. A mutation operator defines
a rewrite rule how certain terms in the programming language are replaced by
mutations. For every occurrence of the term the mutation operator rewrites the
original program into a new mutant. After a set of mutants has been generated,
the test cases are run both on the original and on each mutant. If a test case can
distinguish a mutant from the original program, i.e., a different output behavior
can be observed, we say that this test case kills a mutant. The goal is to develop
a test suite that kills all mutants. This technique of program testing has been
invented by Hamlet [10] and DeMillo et al. [9] in the 70-ies.
Mutation testing has three basic assumptions: (1) the
competent programmer
assumption assumes that programmers make only small errors. This argument
supports the use of small variations in the code to represent the fault models,
i.e., the typical faults of programmers; (2) the chosen
mutation operators
are a
representative set of those errors; (3) via a
coupling effect
, more subtle errors
can be detected by testing against the simple errors only.
