Comparative Assessment of Testing and Model Checking
Using Program Mutation
Jeremy S. Bradbury
Faculty of Science
University of Ontario Institute of Technology
Oshawa, Ontario, Canada
Jeremy.Bradbury@uoit.ca
James R. Cordy, Juergen Dingel2
School of Computing
Queen’s University
Kingston, Ontario, Canada
{cordy, dingel}@cs.queensu.ca
Abstract
Developing correct concurrent code is more difficult
than developing correct sequential code. This difficulty is
due in part to the many different, possibly unexpected, ex-
ecutions of the program, and leads to the need for special
quality assurance techniques for concurrent programs such
as randomized testing and state space exploration. In this
paper an approach is used that assesses testing and for-
mal analysis tools using metrics to measure the effective-
ness and efficiency of each technique at finding concurrency
bugs. Using program mutation, the assessment method
creates a range of faulty versions of a program and then
evaluates the ability of various testing and formal analysis
tools to detect these faults. The approach is implemented
and automated in an experimental mutation analysis frame-
work (ExMAn) which allows results to be more easily repro-
ducible. To demonstrate the approach, we present the re-
sults of a comparison of testing using the IBM tool ConTest
and model checking using the NASA tool Java PathFinder
(JPF).
1. Introduction
In order to fully exploit recent hardware advances such
as multi-core processors, software needs to be concurrent.
In the past, advances in single processors have lead to free
speed-up of sequential programs which will no longer occur
with multi-core technologies. Many imperative program-
ming languages like Java, which are often used in the devel-
opment of sequential programs, can also be used for han-
dling concurrency. For example, Java provides a number
1this work is supported by the Natural Sciences and Engineering Re-
search Council of Canada (NSERC).
2from Jan. to Aug. 2007 on leave to Software Systems Engineering In-
stitute, Braunschweig University of Technology, Braunschweig, Germany.
of synchronization events (wait, notifyAll) for the develop-
ment of concurrent programs. The synchronization events
in Java can affect the scheduling of threads and access to
variables in the shared state [7]. The interleaving space of
a concurrent Java program consists of all possible thread
schedules [12].
The development of concurrent software offers a set of
challenges not present in the development of sequential
code. For example, in software with multiple threads dead-
lock and race conditions can occur. Furthermore, a fault
that leads to a deadlock or race condition may only occur in
a very small number of execution interleavings meaning it is
extremely difficult to detect it prior to software deployment.
Our work focuses primarily on better understanding fault
detection techniques for concurrent software. Many ap-
proaches to ensuring concurrent Java source code is correct
have been proposed including: concurrency testing (e.g.,
ConTest [11]), model checking (e.g., Java PathFinder [15,
22, 1], Bandera/Bogor [19]), dynamic analysis (e.g., Co-
nAn [17]) and static analysis (e.g., FindBug [16]). The
goal of this paper is to compare two existing fault detec-
tion techniques – namely concurrency testing with the IBM
tool ConTest [11] and model checking with NASA’s Java
PathFinder (JPF) [15, 22, 1]. With respect to these two tools
we ask the following questions:
Which technique is more effective?
Which is more efficient?
Effectiveness refers to the ability of each tool to detect con-
currency faults and efficiency refers to how quickly each
tool is capable of finding faults. Our interest in exploring
the relationship between testing and model checking tools
is motivated by a need for improved quality assurance tech-
niques for concurrent industrial source code. Testing has
been an effective industrial technique for fault detection of
sequential programs while model checking tools offer the
potential to substantially aid in the debugging of concurrent
programs.