Searching for liveness property violations in concurrent systems with ACO

ABSTRACT

Liveness properties in concurrent systems are, informally, those properties that stipulate that something good eventually happens during execution. In order to prove that a given system satisfies a liveness property, model checking techniques are utilized. However, most of the model checkers found in the literature use exhaustive deterministic algorithms that require huge amounts of memory if the concurrent system is large. Here we propose the use of an algorithm based on ACOhg, a new kind of Ant Colony Optimization algorithm, for searching for liveness property violations in concurrent systems. We also take into account the structure of the liveness property in order to improve the efficacy and efficiency of the search. The results state that our algorithmic proposal, called ACOhg-live, is able to obtain very short error trails in faulty concurrent systems using a low amount of resources, outperforming by far the results of Nested-DFS and Improved-Nested-DFS, two algorithms used in the literature for this task in the model checking community. This fact makes ACOhg-live a very suitable algorithm for finding liveness errors in large faulty concurrent systems, in which traditional techniques fail because of the model size.

REFERENCES

• 1: Enrique Alba , Francisco Chicano, ACOhg: dealing with huge graphs, Proceedings of the 9th annual conference on Genetic and evolutionary computation, July 07-11, 2007, London, England [doi>10.1145/1276958.1276961]
• 2: 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]
• 3: B. Alpern and F. B. Schneider. Defining liveness. Inform. Proc. Letters, 21:181--185, 1985.
• 4: 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]
• 5: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, January 2000.
• 6: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 7: Marco Dorigo , Thomas Stützle, Ant Colony Optimization, Bradford Book, 2004
• 8: S. Edelkamp, A. L. Lafuente, and S. Leue. Protocol verification with heuristic search. In AAAI-Spring Symposium on Model-based Validation Intelligence, pages 75--83, 2001.
• 9: Stefan Edelkamp , Stefan Leue , Alberto Lluch-Lafuente, Directed explicit-state model checking in the validation of communication protocols, International Journal on Software Tools for Technology Transfer (STTT), v.5 n.2, p.247-267, March 2004 [doi>10.1007/s10009-002-0104-3]
• 10: Rob Gerth , Doron Peled , Moshe Y. Vardi , Pierre Wolper, Simple on-the-fly automatic verification of linear temporal logic, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, p.3-18, June 01, 1995
• 11: 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]
• 12: A. Groce and W. Visser. Heuristics for model checking Java programs. Intl. Jnl. on Software Tools for Technology Transfer, 6(4):260--276, 2004.
• 13: G. J. Holzmann. The SPIN Model Checker. Addison-Wesley, 2004.
• 14: G. J. Holzmann, D. Peled, and M. Yannakakis. On nested depth first search. In Proc. Second SPIN Workshop, pages 23--32, 1996.
• 15: M. Kamel and S. Leue. Validation of a remote object invocation and object migration in CORBA GIOP using Promela/Spin. In Intl. SPIN Workshop, 1998.
• 16: C. C. Michael , G. McGraw , M. A. Schatz, Generating Software Test Data by Evolution, IEEE Transactions on Software Engineering, v.27 n.12, p.1085-1110, December 2001 [doi>10.1109/32.988709]
• 17: D. J. Sheskin. Handbook of Parametric and Nonparametric Statistical Procedures. Chapman & Hall/CRC, 2007.
• 18: Wenhui Zhang, Model Checking Operator Procedures, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.200-215, September 21-24, 1999

INDEX TERMS

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

Additional Classification:
  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.6 Optimization
          Subjects: Global optimization

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

General Terms:
Algorithms, Experimentation, Verification

Keywords:
HSF-SPIN, SPIN, ant colony optimization, liveness properties, metaheuristics