Information Technology Reference
In-Depth Information
an approximation of a system's state space is built from an actual concrete trace.
This is done using an abstraction function; the resulting state space is called an
abstract trace.
Model checking offers the promise of a push-button solution for verification,
and during the last twenty years many researchers have been pursuing that goal.
In practise the technique still suffers from the well known state explosion prob-
lem, i.e. models become too large for analysis. Thus a priority is developing
tractable models by abstracting from the full complexity of the artefact being
verified. Our work in the project on model checking will investigate the inte-
gration of property-based testing and model checking techniques for Erlang. As
model checking inevitably fails to fully verify a piece of software (e.g., due to
state explosion or the problem of constructing an accurate model from a complex
program), we have to resort to testing. But, in fact, testing and model checking
are often complementary techniques. In ProTest we will explore their combina-
tion in model based testing (to provide accurate estimations of space coverage,
to provide a test oracle, etc) and to explore non-exhaustive model checking as
an alternative to testing for highly concurrent and complex distributed systems.
3 Property Discovery
Our work on property discovery covers two main aspects, one dealing with
obtaining properties from a specification, the other dealing with obtaining
properties from a library of existing test cases.
3.1
Properties from Specifications
To enhance how QuickCheck can be applied to other languages, we have pro-
duced a library for testing finite state machines, which has been used in an
industrial project in which the UML design tool Rose/RT was connected to
QuickCheck, allowing systems designed in Rose/RT to be using QuickCheck's
finite state machine library. We have also developed a general approach to test
C software with QuickCheck. In this way, all QuickCheck libraries developed in
the ProTest project also become available to Rose/RT and C programmers.
We have also developed two ways of obtaining properties from specification,
viz. obtaining properties from data type definitions and from databases. The
methods have been evaluated in a number of industrial projects, and some subtle
errors were identified in the financial systems of these companies and the methods
proved useful [ACH08]. The novelty here is that one is assured that the properties
together span the complete set of all possible tests.
Going further we have developed a fully automatic method to generate prop-
erties from purely functional descriptions for both Haskell and Erlang. This tool,
called QuickSpec [Hug08], can automatically generate properties for a given li-
brary of functions. QuickSpec reads in an API of an Erlang module or a Haskell
module, and automatically produces a list of equations that hold for the func-
tions in that module. The method uses random testing to do this (no heavy
