Information Technology Reference
In-Depth Information
As part of the ProTest project, QuickCheck has been extended to so that
it is possible to test an implementation against a finite state machine (rather
than just a simple property). The use of a finite state machine enables the
developer to specify the permitted sequences of program functions, along with
their effect on the data-state of the system. QuickCheck tests an implementation
by selecting random paths through the state machine, with the aim of verifying
their behaviour in the implementation (i.e. checking that pre-/post-conditions
hold on the data state once a transition is executed). Given state-machine model,
QuickCheck can produce the requisite sequences of inputs (with the necessary
data parameters) to automatically test any path in the model against the actual
software system (this is important to with respect to our reverse-engineering
technique described later).
The key problem with model-based techniques such as QuickCheck is the
reliance upon a model that is both accurate and complete. In practice, large
and complex systems are often developed under restrictive time-constraints,
across multiple sites by different developers, and are constantly evolving. Un-
der such circumstances a developer can at best provide a partial model. This is
undermined further as the system evolves due to changes in requirements and
bug-fixes.
2.2 Reverse-Engineering State Machines
Reverse-engineering techniques aim to address this problem. Broadly speaking,
these approaches can be separated into two categories: Those based on source-
code analysis (c.f. [6]), and those based on the analysis of execution traces. Here
we focus on the latter (dynamic) approaches. They are based on the analysis
of program traces, which are sequences of events (e.g. function calls, message-
passing events etc.), that may optionally be annotated with variable values. The
traces can be recorded by instrumenting the source code, or by using tracing
tools. For Erlang several such tools are included in the OTP framework.
From a given set of traces, the challenge for reverse-engineering techniques
is to produce a candidate state machine that conforms to the provided set of
traces. This is not a new problem. Its roots can be traced back to to the 50s,
in Moore's work on “gedanken experiments” on state machines [7] and Nerode's
work on the synthesis of machines from equivalence relations [8]. However it
was Gold's work on Grammar Inference in 1967 that was arguably most influ-
ential, establishing the theoretical limits of regular grammar (i.e. deterministic
state machine) learnability [9]. Most reverse-engineering techniques in the field
of software engineering are inspired by techniques that were initially devised as
grammar-inference techniques [10,11,12,4].
It is unrealistic to expect an inference technique to be able to infer a machine
that is 100% accurate from any arbitrary set of traces. An inference technique
will only produce an accurate result if the provided set of traces is
characteristic
of the behaviour of the underlying software system [11,4]. In terms of state
machines, this must include enough information about what the program can
and cannot do to enable the inference technique to identify every state transition,
