Information Technology Reference
In-Depth Information
Incrementally Discovering Testable
Specifications from Program Executions
Neil Walkinshaw and John Derrick
Department of Computer Science, The University of Sheeld, Sheeld, UK
Abstract.
The ProTest project
1
is an EU FP7 project to develop tech-
niques that improve the testing and verification of concurrent and dis-
tributed software systems. One of the four main work packages is
concerned with the automated identification of specifications that could
serve as a suitable basis for testing; this is currently a tedious and error-
prone manual task that tends to be neglected in practice. This paper
describes how this problem has been addressed in the ProTest project.
It describes a technique that uses test executions to refine the specifi-
cation from which they are generated. It shows how the technique has
been implemented and applied to real Erlang systems. It also describes in
detail the major challenges that remain to be addressed in future work.
1
Introduction
The ProTest project [1] is motivated by the need to develop improved testing
and verification techniques for concurrent and distributed software systems. This
paper describes a particular programme of work within the project that aims
to reverse-engineer testable models. The work is targeted at systems that are
implemented in Erlang [2], and makes use of QuickCheck, the most popular
model-based testing framework for Erlang systems.
Erlang is the leading platform for the development of distributed and concur-
rent software systems. With its Open Telecom Platform (OTP) libraries, Erlang
applications can be rapidly developed and deployed across a large variety of
hardware platforms. This has caused it to become increasingly popular, not only
within large telecoms companies such as Ericsson, but also with a variety of
SMEs in different areas. It is increasingly used to develop applications that are
business-critical, from financial transaction systems (e.g. it forms the basis for
Klarna's services
2
), telephone switches, and web-based communication services.
However, in contrast to the extensive support for rapid program development,
the verification and validation of Erlang systems is to-date largely unsupported.
Consequently there is an inherent danger that important functionality remains
untested and undocumented. The ProTest project is intended to develop a suite
of tools and techniques that help to address this problem.
1
http://www.protest-project.eu
2
http://www.klarna.com
