Information Technology Reference
In-Depth Information
As a part of this effort, we have developed an automated technique to infer
testable specifications from Erlang systems [3]. This does not completely elim-
inate the need for manual intervention - it has to be inspected and perhaps
slightly amended to represent the correct system - but the required effort is
nonetheless substantially reduced. Specifications of the actual system behaviour
can be obtained relatively cheaply; they can serve as a useful guide to under-
standing system behaviour as-is, and can form a suitable basis for regression
testing if the current system behaviour is deemed to be correct.
The technique operates by reverse-engineering a specification from traces of
program executions. As with most techniques that are based on program traces
(referred to as dynamic analysis techniques), the selection of traces is critical
[4]. One of the key novelties of our technique is that, instead of relying on the
developer to record and supply traces, they are obtained automatically by using
a model-based test-set generator. The resulting traces are used to refine the
model at each iteration, until no further tests that contradict the hypothesised
model can be found.
This paper provides details on how the technique works. It shows how the
technique has been combined with an Erlang TCP-testing framework to auto-
matically reverse-engineer a model for a Linux TCP implementation. This is
followed by a substantial discussion of the main areas that need to be addressed
by future work.
2 Background
To provide a motivation for our work, we show in section 2.1 how Erlang appli-
cations are currently tested with the QuickCheck tool, a commonplace Erlang
model-based testing framework. Its weakness is that it currently relies on the
developer to supply the models to be tested. An overview of the challenges of
reverse-engineering models is given in section 2.2.
2.1 Model-Based Testing of Erlang Applications
QuickCheck [5] is an automated model-based testing tool for Erlang. It has
become one of the standard testing tools used by Erlang developers. The 'model'
is conventionally provided by the developer, as a set of simple properties that
must hold for the program to behave correctly, and these have conventionally
been expressed as logical properties in Erlang itself. For example, the following
property would check that the reverse function for lists behaves as expected:
prop_reverse() ->
?FORALL(Xs,list(int()),
lists:reverse(lists:reverse(Xs)) == Xs).
The property prop reverse generates lots of lists of random length, filled with
random integers. For each list (assigned to the variable Xs) it ensures that the
list is the same as the reverse of the reverse. Were this not the case, it would
have found a bug in the lists:reverse function.
