IA159 Formal Verification Methods
Software Testing
Jan Strejˇcek
Department of Computer Science
Faculty of Informatics
Masaryk University
Focus and sources
Focus
software testing is not a typical formal method
we focus on three formal parts of software testing
control flow coverage criteria
dataflow coverage criteria
model-based testing
Sources
Chapter 9 of
D. A. Peled: Software Reliability Methods, Springer, 2001.
Model-based testing.
http://www.goldpractices.com/practices/mbt
IA159 Formal Verification Methods: Software Testing 2/34
Basic classification
Testing can be divided according to
the level of the tested parts
unit (module) testing - the lowest level of testing, where
one tests small pieces of code separately
integration testing - testing that different pieces of code
work well together
system testing - testing the system as a whole
approach to the source code
white box testing (aka transparent box testing)- based on
inspecting the source code
suitable for unit and integration testing
black box testing - does not use the source code (which
may be inaccessible or unknown)
suitable for system testing
IA159 Formal Verification Methods: Software Testing 3/34
Basic terminology
execution path - a path in the flowchart of the tested code, i.e.,
it is a sequence of control points and instructions
appearing in the tested code
test case - a sequence of inputs, actions, and events
accompanied with expected response of the
system
test suite - a set of test cases
IA159 Formal Verification Methods: Software Testing 4/34
White box testing
a typical program has a large or unbounded number of
execution paths
it is not feasible to examine all of them
need for a reasonably small test suite with a high degree of
probability of finding potential errors
code coverage criteria are metrices saying whether a given
test suite covers a given code
testers aim to find the smallest test suite with the highest
coverage
two kinds of code coverage criteria
control flow coverage criteria
dataflow coverage criteria
IA159 Formal Verification Methods: Software Testing 5/34
White box testing
Control flow coverage criteria
IA159 Formal Verification Methods: Software Testing 6/34
Control flow coverage criteria
y:=y+1
x=y and z>w
x:=x−1
true false
When is this code covered?
IA159 Formal Verification Methods: Software Testing 7/34
Control flow coverage criteria
y:=y+1
x=y and z>w
x:=x−1
true false
statement coverage
each executable statement (e.g. assignments, input, test,
output) appears in at least one test case
covering test case: (x = 2, y = 2, z = 4, w = 3)
IA159 Formal Verification Methods: Software Testing 8/34
Control flow coverage criteria
y:=y+1
x=y and z>w
x:=x−1
true false
edge coverage
each execution edge of the flowchart appears in some test
case
two covering test cases: (x = 2, y = 2, z = 4, w = 3),
(x = 3, y = 3, z = 5, w = 7)
IA159 Formal Verification Methods: Software Testing 9/34
Control flow coverage criteria
y:=y+1
x=y and z>w
x:=x−1
true false
condition coverage
each decision predicate is a Boolean combination of
element conditions, e.g. x < y or even(x)
each of these element conditions appears in some test
case where it is calculated to TRUE and in another test
case where it is calculated to FALSE (if possible)
IA159 Formal Verification Methods: Software Testing 10/34
Control flow coverage criteria
y:=y+1
x=y and z>w
x:=x−1
true false
condition coverage
two covering test cases: (x = 3, y = 3, z = 5, w = 7),
(x = 3, y = 4, z = 7, w = 5)
in both cases, the decision predicate is evaluated to
FALSE. . .
IA159 Formal Verification Methods: Software Testing 11/34
Control flow coverage criteria
y:=y+1
x=y and z>w
x:=x−1
true false
edge/condition coverage
executable edges as well as conditions has to be covered
three covering test cases: (x = 2, y = 2, z = 4, w = 3),
(x = 3, y = 3, z = 5, w = 7), (x = 3, y = 4, z = 7, w = 5)
IA159 Formal Verification Methods: Software Testing 12/34
Control flow coverage criteria
y:=y+1
x=y and z>w
x:=x−1
true false
multiple condition coverage
similar to condition coverage
each Boolean combination of TRUE/FALSE values that
may appear in any decision predicate during some
execution of the program must appear in some test case
IA159 Formal Verification Methods: Software Testing 13/34
Control flow coverage criteria
y:=y+1
x=y and z>w
x:=x−1
true false
multiple condition coverage
four covering test cases: (x = 2, y = 2, z = 4, w = 3),
(x = 3, y = 3, z = 5, w = 7), (x = 3, y = 4, z = 7, w = 5),
(x = 3, y = 4, z = 5, w = 6)
disadvantage: an explosion of the number of test cases
IA159 Formal Verification Methods: Software Testing 14/34
Control flow coverage criteria
y:=y+1
x=y and z>w
x:=x−1
true false
path coverage
every executable path must be covered by a test case
the number of paths can be enormous (for example, loops
may result in infinite or an unfeasible number of paths)
IA159 Formal Verification Methods: Software Testing 15/34
Hierarchy of control flow coverage criteria
a criterion A subsumes a criterion B, denoted A → B, if
guaranteeing the coverage A also guarantees B
IA159 Formal Verification Methods: Software Testing 16/34
Hierarchy of control flow coverage criteria
a criterion A subsumes a criterion B, denoted A → B, if
guaranteeing the coverage A also guarantees B
path
coverage

multiple condition
coverage

edge/condition
coverage
uujjjjjjjjjjj

edge
coverage

condition
coverage
statement
coverage
IA159 Formal Verification Methods: Software Testing 17/34
Note
It can happen due to a lucky selection of the test cases, that a
less comprehensive coverage will find errors that a more
comprehensive approach will happen to miss.
IA159 Formal Verification Methods: Software Testing 18/34
Loop coverage
all mentioned criteria (except of path coverage) do not care
about number of loop iterations
ad hoc strategies for testing loops
check the case where the loop is skipped
check the case where the loop is executed once
check the case where the loop is executed some typical
number of times (but what is typical?)
if the bound n on the number of iterations of the loop is
known, try executing it n − 1, n, and n + 1 times
testing loops become even more difficult when nested
loops are involved
IA159 Formal Verification Methods: Software Testing 19/34
White box testing
Dataflow coverage criteria
IA159 Formal Verification Methods: Software Testing 20/34
Dataflow coverage criteria
There may be an execution path in which some variable is set
to some value for a particular purpose, but later the value is
misused. Control flow criteria do not ensure that such an
execution path is included in test suite.
⇓
Dataflow coverage criteria [Rapps-Weyuker, 1985]
IA159 Formal Verification Methods: Software Testing 21/34
Auxiliary sets of nodes
for each program variable x we define the following sets of
flowchart nodes
def(x) = nodes where some value is assigned to x
p−use(x) = nodes where x is used in a predicate (e.g. in if or
while statements)
c−use(x) = nodes where x is used in some expression other
than a predicate
for each s ∈ def(x) we further define the sets
dpu(s, x) = nodes s ∈ p−use(x) such that there is a path
from s to s going only through nodes not included
in def(x)
dcu(s, x) = nodes s ∈ c−use(x) such that there is a path
from s to s going only through nodes not included
in def(x)
IA159 Formal Verification Methods: Software Testing 22/34
Dataflow coverage criteria
For each program variable x and each node s ∈ def(x), the
test suite should include the following paths starting in s and
going only through nodes not included in def(x), as subpaths:
all-defs: include one path to some node in dpu(s, x) or in
dcu(s, x).
all-p-uses: include one path to each node in dpu(s, x).
all-c-uses/some-p-uses: include one path to each node in
dcu(s, x), but if dcu(s, x) is empty, include at least
one path to some node in dpu(s, x).
all-p-uses/some-c-uses: include one path to each node in
dpu(s, x), but if dpu(s, x) is empty, include at least
one path to some node in dcu(s, x).
all-uses: include one path to each node in dpu(s, x) and to
each node in dcu(s, x).
all-du-paths: include all the paths to each node in dpu(s, x)
and to each node in dcu(s, x).
IA159 Formal Verification Methods: Software Testing 23/34
Dataflow coverage criteria
The paths should not contain cycles except for the first and the
last nodes, which may be the same (e.g. an assignment
x := x + 1 is both in def(x) and c−use(x)).
IA159 Formal Verification Methods: Software Testing 24/34
Hierarchy of dataflow coverage criteria
all-du-paths
coverage

all-uses
coverage
xxqqqqqqqq
&&MMMMMMMM
all-c-uses/some-p-uses
coverage

all-p-uses/some-c-uses
coverage
sshhhhhhhhhhhhhhhhhhh

all-defs
coverage
all-p-uses
coverage
IA159 Formal Verification Methods: Software Testing 25/34
Notes
we cannot expect that our test suite achieves the full
coverage (for example, some instructions may be
unreachable)
we cannot even compute the maximal possible coverage
as it is undecidable whether a given part of the code is
reachable or not
there are other approaches to evaluation quality of a test
suite, e.g. mutation analysis
[Budd-DeMillo-Lipton-Frederick, POPL’80]
IA159 Formal Verification Methods: Software Testing 26/34
Mutation analysis
Idea
A test suite is unlikely to be comprehensive enough if it gives
the same results to two different programs.
given a test suite and a code, one generates several
mutations of the program (based on code inspections and
structural changes)
if some test case behaves differently on the original code
and a mutation, then the mutation dies
if a considerable number of mutations remain alive, the test
suite is probably inappropriate
IA159 Formal Verification Methods: Software Testing 27/34
Notes (cont.)
addition of a code monitoring executions of test cases (e.g.
a code measuring the coverage) can affect a behaviour of
the system under test
there are dedicated software packages for test case
generation, coverage evaluation, test execution, and test
management (maintaining different test suits, perform
version control etc.)
IA159 Formal Verification Methods: Software Testing 28/34
Black box testing
Model-based testing
IA159 Formal Verification Methods: Software Testing 29/34
Black box testing: model-based testing
to check the functionality of the system under test, we
need to know the intended behaviour of the system
the behaviour can be described by
simple text
message sequence charts
state machines
. . .
formal descriptions are called models of the system
IA159 Formal Verification Methods: Software Testing 30/34
Example: A model of a simple phone system
IA159 Formal Verification Methods: Software Testing 31/34
Model-based testing: coverage criteria
models can be used to generate a test cases
a test suite can be designed according to various coverage
criteria
cover all edges
cover all the states
cover all the paths (usually impractical)
cover each adjacent sequence of n states
cover certain nodes at least/at most a given number of
times in each test case
switch coverage - cover each pair of incoming and
outcoming edge for all states
after execution of the test suite and evaluation of the
obtained results, we decide whether to
modify the model or
generate more tests or
stop testing
IA159 Formal Verification Methods: Software Testing 32/34
Probabilistic testing
we may want to test primarily the typical executions in
order to maximize minimal time to failure (MTTF)
in this case we employ probabilistic testing
the system is modeled as a Markov chain
the test suite is then generated according to probabilities of
transitions
IA159 Formal Verification Methods: Software Testing 33/34
Coming next week
Deductive software verification
prehistory of formal verification: 40 years old technique!
Does my program terminate? For all inputs?
If yes, does it do what it is supposed to do?
Can it be proven automatically?
IA159 Formal Verification Methods: Software Testing 34/34