Information Technology Reference
In-Depth Information
below, where there are five valid traces, and one trace that has been found to be
impossible / invalid. The “prefix acceptor” that is generated from these traces
is shown to the left, below the traces. The process of selecting state pairs to be
merged (as carried out by the
selectStateP air
function) is illustrated with a
selection of examples. Pair (
b, f
) produce a high score of 5; by tracing out the
sub-trees from both states there are 5 matching labels in the outgoing sub-trees.
On the other hand, pair (
b, c
) produce a score of -1, because a “close” is possible
from b, but not from c. Any pair that involves node
a
produces a score of 0,
because a “load” only appears once in the machine and cannot be matched to
any other edges in the tree. Thus, we would begin by merging pair (
b, f
), which
would lead to the machine shown to the right of the original prefix tree, and the
search begins for the next pair of states to merge.
3.2 Automating Trace Collection for the EDSM Algorithm with
QuickCheck
When using traces to reverse-engineer state machines (or any other type of
model), the key challenge is to supply the technique with a suitable set of traces.
The sheer number of traces required, and the prior knowledge and time on the
part of the user that is required to execute these traces, often renders the task
infeasible in practice [4]. The technique that is presented here addresses this
problem; it requires no traces from the user, and shows how QuickCheck can be
used to automatically gather traces.
Instead of starting with a set of traces, we begin simply with the set of possible
inputs or functions that are to label the transitions in the final state machine
(i.e. the set
Σ
in the LTS), and also supply the program that is to be tested.
Our technique generates the most basic possible state machine from
Σ
-asingle
state with a loop that is labelled by every element in
Σ
. This is translated into
a corresponding QuickCheck specification, and QuickCheck attempts to execute
a set of random tests that are generated from this general machine. Invariably,
tests will disagree with the model (i.e. a test may fail, but be deemed valid
by the hypothesis model or vice versa); these are recorded and fed into the
EDSM algorithm, which produces a more refined model. This is in turn used
to generate more tests, which produce a more refined model, and the iterative
process continues until QuickCheck can find no further tests that disagree with
the model.
The algorithm is displayed in algorithm 2. The notation
L
LTS
refers to the
language
of the hypothesis LTS. If a sequence belongs to the language, it repre-
sents a sequence of events that should be permitted according to the LTS. The
runT est
function refers to QuickCheck executing a test, and
generateTests
refers to the automated random test set generation process implemented by
QuickCheck. The process broadly consists of executing the tests, observing if
they pass or fail, and then checking (in lines 8 and 14) whether these are in
agreement with the hypothesis LTS.
A QuickCheck state machine specification consists of more than just an LTS.
It corresponds to an extended state machine [20]; for each element in
Σ
it can
