Article

Exploring Very Large State Spaces Using Genetic Algorithms

Authors:

Patrice Godefroid,

Sarfraz KhurshidAuthors Info & Claims

TACAS '02: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

Pages 266 - 280

Published: 08 April 2002 Publication History

Abstract

We present a novel frameworkfor exploring very large state spaces of concurrent reactive systems. Our frameworkexploits application-independent heuristics using genetic algorithms to guide a state-space search towards error states. We have implemented this frameworkin conjunction with VeriSoft, a tool for exploring the state spaces of software applications composed of several concurrent processes executing arbitrary code. We present experimental results obtained with several examples of programs, including a C implementation of a publickey authentication protocol.We discuss heuristics and properties of state spaces that help a genetic search detect deadlocks and assertion violations. For finding errors in very large state spaces, our experiments show that a genetic search using simple heuristics can significantly outperform random and systematic searches.

References

[1]

B. Boigelot and P. Godefroid. Model checking in practice: An analysis of the ACCESS.bus protocol using SPIN. In Proceedings of Formal Methods Europe'96 , volume 1051 of Lecture Notes in Computer Science , pages 465-478, Oxford, March 1996. Springer-Verlag.

[2]

Paul Marcos Siqueira Bueno and Mario Jino. Identification of potentially infeasible program paths by monitoring the search for test data. In Proceedings of the 15th IEEE International Conference on Automated Software Engineering (ASE) , Grenoble, France, September 2000.

[3]

E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Futurebus+ cache coherence protocol. In Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and Their Apllications . North-Holland, 1993.

[4]

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking . The MIT Press, Cambridge, MA, 1999.

[5]

S. Edelkamp, A. L. Lafuente, and S. Leue. Directed explicit model checking with hsf-spin. In Proceedings of the 2001 SPIN Workshop , volume 2057 of Lecture Notes in Computer Science , pages 57-79. Springer-Verlag, 2001.

[6]

A. E. Eiben, R. Hinterding, and Z. Michalewicz. Parameter control in evolutionary algorithms. IEEE Transactions on Evolutionary Computation , 3(2):124-141, 1999.

[7]

Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem , volume 1032 of Lecture Notes in Computer Science . Springer-Verlag, January 1996.

[8]

Patrice Godefroid. Model checking for programming languages using VeriSoft. In Proceedings of the 24th Annual ACM Symposium on the Principles of Programming Languages (POPL) , pages 174-186, Paris, France, January 1997.

[9]

Patrice Godefroid, Robert Hanmer, and Lalita Jagadeesan. Model Checking Without a Model: An Analysis of the Heart-Beat Monitor of a Telephone Switch using VeriSoft. In Proceedings of ACM SIGSOFT ISSTA'98 (International Symposium on Software Testing and Analysis) , pages 124-133, Clearwater Beach, March 1998.

[10]

David E. Goldberg. Genetic Algorithms in Search, Optimization, and Machine Learning . Addison-Wesley Publishing Company, Inc., Reading, MA, 1989.

[11]

John Holland. Adaptation in Natural and Artificial Systems . The University of Michigan Press, Ann Arbor, MI, 1975.

[12]

B. F. Jones, H. H. Sthamer, and D. E. Eyres. Automatic structural testing using genetic algorithms. Software Engineering Journal , pages 299-306, Sep 1996.

[13]

Sarfraz Khurshid. Testing an intentional naming system using genetic algorithms. In Proceedings of the 7th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS) , Genova, Italy, April 2001.

[14]

Gavin Lowe. An attackon the Needham-Schroeder public-key authentication protocol. Information Processing Letters , 1995.

[15]

Roger Needham and Michael Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM , 21(12):993-999, 1978.

[16]

Roy P. Pargas, Mary Jean Harrold, and Robert Peck. Test-data generation using genetic algorithms. Journal of Software Testing, Verification, and Reliability , 9(4):263-282, 1999.

[17]

Ingo Rechenberg. Evolutionsstrategie: Optimierung technischer Systeme nach Prinzipien der biologischen Evolution . Frommann-Holzbog, Stuttgart, 1973.

[18]

Peter Ross and Dave Corne. Applications of genetic algorithms. AISB Quaterly on Evolutionary Computation , pages 23-30, Autumn 1994.

[19]

H. Rudin. Protocol development success stories: Part I. In Proc. 12th IFIP WG 6.1 International Symposium on Protocol Specification, Testing, and Verification , Lake Buena Vista, Florida, June 1992. North-Holland.

[20]

Nicol N. Schraudolph and Richard K. Belew. Dynamic parameter encoding for genetic algorithms. Machine Learning , 9(1):9-21, 1992.

[21]

C. H. Yang. Prioritized Model Checking . PhD thesis, Stanford University, 1998.

Cited By

Milewicz RPirkelbauer P(2017)Refinement of structural heuristics for model checking of concurrent programs through data miningComputer Languages, Systems and Structures10.1016/j.cl.2016.06.00147:P2(170-188)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1016/j.cl.2016.06.001
Francesco NLettieri GSantone AVaglini G(2016)Heuristic search for equivalence checkingSoftware and Systems Modeling (SoSyM)10.1007/s10270-014-0416-215:2(513-530)Online publication date: 1-May-2016
https://dl.acm.org/doi/10.1007/s10270-014-0416-2
Baluda MVos TEldh SPrasetya W(2015)EvoSE: evolutionary symbolic executionProceedings of the 6th International Workshop on Automating Test Case Design, Selection and Evaluation10.1145/2804322.2804325(16-19)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2804322.2804325
Show More Cited By

Exploring Very Large State Spaces Using Genetic Algorithms
1. Computing methodologies
  1. Artificial intelligence
    1. Search methodologies
2. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Exploring very large state spaces using genetic algorithms

We present a novel framework for exploring very large state spaces of concurrent reactive systems. Our framework exploits application-independent heuristics using genetic algorithms to guide a state-space search toward error states. We have implemented ...
Partial-order reduction for general state exploring algorithms

Partial-order reduction is one of the main techniques used to tackle the combinatorial state explosion problem occurring in explicit-state model checking of concurrent systems. The reduction is performed by exploiting the independence of concurrently ...
Explorative steady state genetic algorithms and elitist genetic algorithms for optimal reactive power planning
AIKED'09: Proceedings of the 8th WSEAS international conference on Artificial intelligence, knowledge engineering and data bases

This paper presents the comparative performances between a computationally enhanced steady state genetic algorithm (CSGA), standard steady state genetic algorithms (SSGA) and elitist genetic algorithms (EGA) in improving the voltage profile and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

TACAS '02: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

April 2002

480 pages

ISBN:3540434194

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 08 April 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

34
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Milewicz RPirkelbauer P(2017)Refinement of structural heuristics for model checking of concurrent programs through data miningComputer Languages, Systems and Structures10.1016/j.cl.2016.06.00147:P2(170-188)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1016/j.cl.2016.06.001
Francesco NLettieri GSantone AVaglini G(2016)Heuristic search for equivalence checkingSoftware and Systems Modeling (SoSyM)10.1007/s10270-014-0416-215:2(513-530)Online publication date: 1-May-2016
https://dl.acm.org/doi/10.1007/s10270-014-0416-2
Baluda MVos TEldh SPrasetya W(2015)EvoSE: evolutionary symbolic executionProceedings of the 6th International Workshop on Automating Test Case Design, Selection and Evaluation10.1145/2804322.2804325(16-19)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2804322.2804325
Poulding SFeldt REsparcia-Alcázar A(2015)Heuristic Model Checking using a Monte-Carlo Tree Search AlgorithmProceedings of the 2015 Annual Conference on Genetic and Evolutionary Computation10.1145/2739480.2754767(1359-1366)Online publication date: 11-Jul-2015
https://dl.acm.org/doi/10.1145/2739480.2754767
Francesco NLettieri GSantone AVaglini G(2014)GreASEACM Transactions on Software Engineering and Methodology10.1145/256056323:3(1-26)Online publication date: 2-Jun-2014
https://dl.acm.org/doi/10.1145/2560563
Poskitt CPoulding S(2013)Using Contracts to Guide the Search-Based Verification of Concurrent ProgramsProceedings of the 5th International Symposium on Search Based Software Engineering - Volume 808410.5555/2946711.2946737(263-268)Online publication date: 24-Aug-2013
https://dl.acm.org/doi/10.5555/2946711.2946737
Aizatulin MGordon AJürjens JYu TDanezis GGligor V(2012)Computational verification of C protocol implementations by symbolic executionProceedings of the 2012 ACM conference on Computer and communications security10.1145/2382196.2382271(712-723)Online publication date: 16-Oct-2012
https://dl.acm.org/doi/10.1145/2382196.2382271
Pelayo FCuartero FCazorla D(2011)Looking for a cheaper ROSAProceedings of the 11th international conference on Artificial neural networks conference on Advances in computational intelligence - Volume Part II10.5555/2023332.2023387(380-387)Online publication date: 8-Jun-2011
https://dl.acm.org/doi/10.5555/2023332.2023387
Binkley DHarman MLakhotia K(2011)FlagRemoverACM Transactions on Software Engineering and Methodology10.1145/2000791.200079620:3(1-33)Online publication date: 26-Aug-2011
https://dl.acm.org/doi/10.1145/2000791.2000796
Aizatulin MDupressoir FGordon AJürjens J(2011)Verifying cryptographic code in cProceedings of the 8th international conference on Formal Aspects of Security and Trust10.1007/978-3-642-29420-4_1(1-20)Online publication date: 12-Sep-2011
https://dl.acm.org/doi/10.1007/978-3-642-29420-4_1
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents