Observations in using parallel and sequential evolutionary algorithms for automatic software testing
Enrique Alba∗ , Francisco Chicano
Grupo GISUM, Dept. de Lenguajes y Ciencias de la Computación, University of Málaga, Spain Available online 7 February 2007
Abstract In this paper we analyze the applicationof parallel and sequential evolutionary algorithms (EAs) to the automatic test data generation problem. The problem consists of automatically creating a set of input data to test a program. This is a fundamental step in software development and a time consuming task in existing software companies. Canonical sequential EAs have been used in the past for this task. We explore here the use of parallelEAs. Evidence of greater efﬁciency, larger diversity maintenance, additional availability of memory/CPU, and multi-solution capabilities of the parallel approach, reinforce the importance of the advances in research with these algorithms. We describe in this work how canonical genetic algorithms (GAs) and evolutionary strategies (ESs) can help in software testing, and what the advantages are (ifany) of using decentralized populations in these techniques. In addition, we study the inﬂuence of some parameters of the proposed test data generator in the results. For the experiments we use a large benchmark composed of twelve programs that includes fundamental algorithms in computer science. 2007 Elsevier Ltd. All rights reserved.
Keywords: Software testing; Evolutionary algorithms;Evolutionary testing; Parallel evolutionary algorithms
1. Introduction From the very beginning of computer research, computer engineers have been interested in techniques allowing them to know whether a software module fulﬁlls a set of requirements (the speciﬁcation). Modern software is very complex and these techniques have become a need in most software companies. One of these techniques is formalveriﬁcation, in which some properties of the software can be checked much like a mathematical theorem deﬁned on the source code. Two very well-known logics used in this veriﬁcation are predicate calculus [1,2] and Hoare logic . However, formal veriﬁcation using logics is not fully automatic. Although automatic theorem provers can assist the process, human intervention is still needed. Anotherwell-known and fully automatic formal method is model checking . In this case all the possible program states are analyzed (in a direct or indirect way) in order to prove that the program satisﬁes a given property. This property is speciﬁed using a temporal logic like LTL  or CTL . Both in formal veriﬁcation and model checking a model of the program is required in order to prove (or refute)the properties we want to check. In order to ensure that the model correctly captures the behavior of the program, some reﬁnement-based approach is needed along the development process. One of the best known model checkers is SPIN , which takes a software model codiﬁed in PROMELA (a programming language usually not used in real programs) and a property
∗ Corresponding author.
E-mailaddresses: firstname.lastname@example.org (E. Alba), email@example.com (F. Chicano). 0305-0548/$ - see front matter doi:10.1016/j.cor.2007.01.016 2007 Elsevier Ltd. All rights reserved.
E. Alba, F. Chicano / Computers & Operations Research 35 (2008) 3161 – 3183
speciﬁed in LTL as input. The drawback of using the PROMELA language is currently solved by the use of translations tools such as the oneintegrated in the Bandera tool kit  or the one described in , which translates Java code into the intermediate language accepted by SAL model checker . However, we can also ﬁnd model checkers like Java PathFinder , which in its last versions directly works on bytecodes of multi-threaded Java programs. The main drawback of a model checking approach is the so-called state explosion: when...