Model checking Java programs using structural heuristics

ABSTRACT

We describe work in troducing heuristic search into the Java PathFinder model checker, which targets Java bytecode. Rather than focusing on heuristics aimed at a particular kind of error (such as deadlocks) we describe heuristics based on a modification of traditional branch coverage metrics and other structure measures, such as thread inter-dependency. We present experimental results showing the utility of these heuristics, and argue for the usefulness of structural heuristics as a class.

REFERENCES

• 1: Paul E. Ammann , Paul E. Black , William Majurski, Using Model Checking to Generate Tests from Specifications, Proceedings of the Second IEEE International Conference on Formal Engineering Methods, p.46, December 09-11, 1998
• 2: P. Ammann and P. Black. Test Generation and Recognition with Formal Methods. In Proceedings of the 1st International workshop on Automated Program Analysis, Testing, and Verication, pages 64-67, 2000.
• 3: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 4: Boris Beizer, Software testing techniques (2nd ed.), Van Nostrand Reinhold Co., New York, NY, 1990
• 5: Roderick Bloem , Kavita Ravi , Fabio Somenzi, Symbolic guided search for CTL model checking, Proceedings of the 37th conference on Design automation, p.29-34, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337306]
• 6: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 7: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 8: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 9: Jamieson M. Cobleigh , Lori A. Clarke , Leon J. Osterweil, The right algorithm at the right time: comparing data flow analysis algorithms for finite state verification, Proceedings of the 23rd International Conference on Software Engineering, p.37-46, May 12-19, 2001, Toronto, Ontario, Canada
• 10: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 11: Matthew B. Dwyer , John Hatcliff , Roby Joehanes , Shawn Laubach , Corina S. Păsăreanu , Hongjun Zheng , Willem Visser, Tool-supported program abstraction for finite-state verification, Proceedings of the 23rd International Conference on Software Engineering, p.177-187, May 12-19, 2001, Toronto, Ontario, Canada
• 12: Stefan Edelkamp , Alberto Lluch Lafuente , Stefan Leue, Directed explicit model checking with HSF-SPIN, Proceedings of the 8th international SPIN workshop on Model checking of software, p.57-79, May 2001, Toronto, Ontario, Canada
• 13: Alberto Lluch-Lafuente , Stefan Edelkamp , Stefan Leue, Partial Order Reduction in Directed Model Checking, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, p.112-127, April 11-13, 2002
• 14: S. Edelkamp, A. L. Lafuente, and S. Leue. Trail-Directed Model Checking. In Proceedings of the Workshop of Software Model Checking, Electrical Notes in Theoretical Computer Science, Elsevier, July 2001.
• 15: Patrice Godefroid, VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software, Proceedings of the 9th International Conference on Computer Aided Verification, p.476-479, June 22-25, 1997
• 16: Patrice Godefroid , Sarfraz Khurshid, Exploring Very Large State Spaces Using Genetic Algorithms, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.266-280, April 08-12, 2002
• 17: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 18: Alex Groce , Willem Visser, Heuristic Model Checking for Java Programs, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, p.242-245, April 11-13, 2002
• 19: P. E. Hart, N. J. Nilsson and B. Raphael. A formal basis for heuristic determination of minimum path cost. In IEEE Transactions Syst. Science and Cybernetics, 4(2):100-107, 1968.
• 20: K. Havelund, M. Lowry, S. Park, C. Pecheur, J. Penix, W. Visser and J. White. Formal Analysis of the Remote Agent Before and After Flight. In Proceedings of the 5th NASA Langley Formal Methods Workshop, June 2000, 2000.
• 21: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 22: G. J. Holzmann. Algorithms for automated protocol verification. AT&T Technical Journal, 69(2):32-44, Feb. 1990, pages 32-44. Special Issue on Protocol Testing, Specification, and Verification.
• 23: Gerard J. Holzmann , Doron Peled, The State of SPIN, Proceedings of the 8th International Conference on Computer Aided Verification, p.385-389, August 03, 1996
• 24: G. J. Holzmann and M. H. Smith. Automating Software Feature Verification. In Bell Labs Technical Journal, 5(2);72-87 April-June 2000
• 25: Claudio Demartini , Radu Iosif , Riccardo Sisto, dSPIN: A Dynamic Extension of SPIN, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.261-276, September 21-24, 1999
• 26: F. J. Lin, P. M. Chu, and M. T. Liu. Protocol Verification Using Reachability Analysis: The State Space Explosion Problem and Relief Strategies. ACM, 126-135, 1988.
• 27: Corina S. Pasareanu , Matthew B. Dwyer , Willem Visser, Finding Feasible Counter-examples when Model Checking Abstracted Java Programs, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.284-298, April 02-06, 2001
• 28: John Penix , Willem Visser , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verification of time partitioning in the DEOS scheduler kernel, Proceedings of the 22nd international conference on Software engineering, p.488-497, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337364]
• 29: A. Pretschner. Classical search strategies for test case generation with Constraint Logic Programming. In Proceedings of the Workshop on Formal Approaches to Testing of Software, pages 47-60, 2001.
• 30: RTCA Special Committee 167. Software considerations in airborne systems and equipment certification. Technical Report DO-178B, RTCA, Inc., Dec. 1992.
• 31: Hassen Saïdi, Modular and Incremental Analysis of Concurrent Software Systems, Proceedings of the 14th IEEE international conference on Automated software engineering, p.92, October 12-15, 1999
• 32: N. Tracey , J. Clark , K. Mander , J. McDermid, An Automated Framework for Structural Test-Data Generation, Proceedings of the 13th IEEE international conference on Automated software engineering, p.285, October 13-16, 1998
• 33: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 34: William Visser , SeungJoon Park , John Penix, Using predicate abstraction to reduce object-oriented programs for model checking, Proceedings of the third workshop on Formal methods in software practice, p.3-182, August 2000, Portland, Oregon, United States [doi>10.1145/349360.351125]
• 35: C. Han Yang , David L. Dill, Validation with guided search of the state space, Proceedings of the 35th annual conference on Design automation, p.599-604, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277201]

INDEX TERMS

Keywords:
coverage metrics, heuristics, model checking, testing