Recall that a state is
a particular assignment of values to the program variables. Finite programs usually
have a small number of variables with finite domains: Booleans, enumerations, or
small integers. The variables of ???infinite??? model programs have ???infinite??? domains:
numbers, strings, or richer data types.
To explore ???infinite??? model programs, we must resort to finitization: execute a
finite subset of method calls (including parameters) that we judge to be representative
for the purposes of a particular analysis. Exploration with finitization generates an
FSM that is an approximation of the huge true FSM that represents all possible
behaviors of the model program. Although an approximation is not complete, it can
be farmore thorough than is usually achievedwithout this level of automation. Along
with abstraction and choosing feature subsets, approximation makes it feasible to
analyze large, complex systems.
We provide many different techniques for achieving finitization by pruning or
sampling, where the analyst can define rules for limiting exploration. Much of the
analyst??™s skill involves choosing a finitization technique that achieves meaningful
coverage or probes particular issues.
1.3 Model-based testing
Model-based testing is testing based on a model that describes how the program is
supposed to behave. The model is used to automatically generate the test cases, and
can also be used as the oracle that checks whether the implementation under test
(IUT) passes the tests.
Pages:
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34