Information Technology Reference
In-Depth Information
and to distinguish between every pair of non-equivalent states. Thus the key
challenges lie in (a)
identifying
the relevant subset of executions and (b)
col lecting
them - a potentially expensive and time-consuming process.
Current reverse-engineering techniques force the user to make a di
cult com-
promise between accuracy and practical applicability. On the one hand, there
are several
passive
inference techniques [10,13,14] that are reasonably easy to
apply and cheap to use, but these can result in inaccurate models unless the
user has a prior comprehensive knowledge of the system that can be used to
obtain required set of traces [4]. On the other hand, they can choose
active
in-
ference techniques (e.g. based on Angluin's
L
∗
algorithm [15,16]), that guarantee
an accurate model, but are usually prohibitively expensive and fail to scale to
larger, more complex systems.
3 An Iterative, Test-Driven Model Inference Approach
This section describes a specification inference technique that was developed by
the authors as part of the ProTest project [3]. It circumvents the problems that
are intrinsic to conventional passive approaches. It does not rely on a human user
to supply it with traces, but instead resorts to a model-based test set generator
to identify and collect the traces automatically. The model from which these
tests are generated is updated and refined with each iteration, until no more
tests can be found that conflict with the model.
The approach is underpinned by the Erlang QuickCheck tool described in sec-
tion 2.1. The presented technique will infer state machine transition structures,
which are represented as Labelled Transition Systems. An LTS
3
is a quadru-
ple
A
=(
Q, Σ, δ, q
0
), where
Q
is a finite set of states,
Σ
is a finite alphabet,
δ
:
Q
×
Σ
→
Q
is a partial function and
q
0
∈
Q
. In this work we assume that an
LTS is deterministic.
The rest of this section describes the basic (passive) algorithm that can be
used to infer state machines from traces. We use the EDSM Blue-Fringe algo-
rithm [17]. This is followed by a description of how the EDSM algorithm can be
combined with the QuickCheck testing framework, so that traces are automati-
cally extracted from the subject system.
3.1
Inferring State Machines from Traces
We begin by describing the underlying algorithm for inferring state machines
from traces. State machine inference techniques in the software engineering do-
main tend to use the
k
-tails algorithm [10,18]. This is however prone to several
weaknesses (see previous work by the authors [4]). Instead we use the more re-
cent EDSM algorithm that has emerged from the closely related field of regular
grammar inference [17].
The EDSM algorithm is presented in Algorithm 1. The algorithm works on
the basis of two types of trace: a set
Pos
of traces that represent valid program
3
References to “state machines” are henceforth assumed to refer to their LTS.
