Finding deadlocks in large concurrent java programs using genetic algorithms

ABSTRACT

Model checking is a fully automatic technique for checking concurrent software properties in which the states of a concurrent system are explored in an explicit or implicit way. However, the state explosion problem limits the size of the models that are possible to check. Genetic Algorithms (GAs) are metaheuristic techniques that have obtained good results in problems in which exhaustive techniques fail due to the size of the search space. Unlike exact techniques, metaheuristic techniques cannot be used to verify that a program satisfies a given property, but they can find errors on the software using a lower amount of resources than exact techniques. In this paper, we compare a GA against classical exact techniques and we propose a new operator for this problem, called memory operator, which allows the GA to explore even larger search spaces. We implemented our ideas in the Java PathFinder (JPF) model checker to validate them and present our results. To the best of our knowledge, this is the first implementation of a Genetic Algorithm in this model checker.

REFERENCES

• 1: Enrique Alba , Francisco Chicano, Finding safety errors with ACO, Proceedings of the 9th annual conference on Genetic and evolutionary computation, July 07-11, 2007, London, England [doi>10.1145/1276958.1277171]
• 2: Enrique Alba , José M. Troya, Genetic Algorithms for Protocol Validation, Proceedings of the 4th International Conference on Parallel Problem Solving from Nature, p.870-879, September 22-26, 1996
• 3: Christian Blum , Andrea Roli, Metaheuristics in combinatorial optimization: Overview and conceptual comparison, ACM Computing Surveys (CSUR), v.35 n.3, p.268-308, September 2003 [doi>10.1145/937503.937505]
• 4: Jerry R. Burch , Edmund M. Clarke , David E. Long , Kenneth L. McMillan , David L. Dill, Symbolic Model Checking for Sequential Circuit Verification, Carnegie Mellon University, Pittsburgh, PA, 1993
• 5: E. Clarke, O. Grumberg, M. Minea, and D. Peled. State space reduction using partial order techniques. International Journal on Software Tools for Technology Transfer (STTT), 2(3):279--287, 1999.
• 6: Edsger W. Dijkstra, Hierarchical ordering of sequential processes, The origin of concurrent programming: from semaphores to remote procedure calls, Springer-Verlag New York, Inc., New York, NY, 2002
• 7: Patrice Godefroid , Sarfraz Khurshid, Exploring very large state spaces using genetic algorithms, International Journal on Software Tools for Technology Transfer (STTT), v.6 n.2, p.117-127, August 2004 [doi>10.1007/s10009-004-0141-1]
• 8: Ganesh Gopalakrishnan, Computation Engineering: Applied Automata Theory and Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 9: A. Groce and W. Visser. Heuristics for model checking java programs. International Journal on Software Tools for Technology Transfer (STTT), 6(4):260--276, 2004.
• 10: Dan Gusfield , Robert W. Irving, The stable marriage problem: structure and algorithms, MIT Press, Cambridge, MA, 1989
• 11: A. L. Lafuente. Symmetry reduction and heuristic search for error detection in model checking. Workshop on Model Checking and Artificial Intelligence, August 2003.
• 12: Leslie Lamport, Verification and Specifications of Concurrent Programs, A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium, p.347-374, June 01-04, 1993
• 13: D. J. Sheskin. Handbook of Parametric and Nonparametric Statistical Procedures. Chapman & Hall/CRC, 2007.
• 14: M. Yagiura and T. Ibaraki. On metaheuristic algorithms for combinatorial optimization problems. Systems and Computers in Japan, 32(3):33--55, 2001.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.8 Problem Solving, Control Methods, and Search
          Subjects: Heuristic methods

General Terms:
Verification

Keywords:
genetic algorithm, graph search, memory operator, model checking