ABSTRACT
Symbolic execution is a popular technique for automatically generating test cases achieving high structural coverage. Symbolic execution suffers from scalability issues since the number of symbolic paths that need to be explored is very large (or even infinite) for most realistic programs. To address this problem, we propose a technique, Simple Static Partitioning, for parallelizing symbolic execution. The technique uses a set of pre-conditions to partition the symbolic execution tree, allowing us to effectively distribute symbolic execution and decrease the time needed to explore the symbolic execution tree. The proposed technique requires little communication between parallel instances and is designed to work with a variety of architectures, ranging from fast multi-core machines to cloud or grid computing environments. We implement our technique in the Java PathFinder verification tool-set and evaluate it on six case studies with respect to the performance improvement when exploring a finite symbolic execution tree and performing automatic test generation.
We demonstrate speedup in both the analysis time over finite symbolic execution trees and in the time required to generate tests relative to sequential execution, with a maximum analysis time speedup of 90x observed using 128 workers and a maximum test generation speedup of 70x observed using 64 workers.
- P. E. Ammann, P. E. Black, and W. Majurski. Using model checking to generate tests from specifications. In Proc. of 2nd IEEE Int'l. Conference on Formal Engineering Methods, pages 46--54. IEEE Computer Society, Nov. 1998. Google ScholarDigital Library
- S. Anand, C. Pasareanu, and W. Visser. JPF-SE: A symbolic execution extension to Java PathFinder. In Proc. of 13th TACAS Conference, volume 4424, page 134. Springer, 2007. Google ScholarDigital Library
- J. Barnat, L. Brim, and J. Chaloupka. Parallel breadth-first search LTL model-checking. In Proc. of 18th IEEE Int'l. Conference on Automated Software Engineering, pages 106--115, 2003.Google ScholarDigital Library
- B. Bezier. Software Testing Techniques, 2nd Edition. Van Nostrand Reinhold, New York, 1990. Google ScholarDigital Library
- C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated Testing Based on Java Predicates. In Proc. of the 2002 ACM SIGSOFT Int'l. Symposium on Software Testing and Analysis, pages 123--133. ACM New York, NY, USA, 2002. Google ScholarDigital Library
- J. Chilenski and S. Miller. Applicability of modified condition/decision coverage to software testing. Software Engineering Journal, 9:193--200, September 1994.Google ScholarCross Ref
- L. Ciortea, C. Zamfir, S. Bucur, V. Chipounov, and G. Candea. Cloud9: A Software Testing Service.Google Scholar
- T. Downing. Java RMI: remote method invocation. IDG Books Worldwide, Inc. Foster City, CA, USA, 1998. Google ScholarDigital Library
- M. Dwyer, S. Elbaum, S. Person, and R. Purandare. Parallel randomized state-space search. In Proc of 29th Int'l. Conference on Software Engineering, pages 3--12, 2007. Google ScholarDigital Library
- B. Elkarablieh, D. Marinov, and S. Khurshid. Efficient solving of structural constraints. In Proc. of the 2008 International Symposium on Software Testing and Analysis, pages 39--50. ACM New York, NY, USA, 2008. Google ScholarDigital Library
- P. Godefroid. Compositional dynamic test generation. In Proc. of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 47--54. ACM New York, NY, USA, 2007. Google ScholarDigital Library
- G. Holzmann and D. Bosnacki. The design of a multicore extension of the spin model checker. IEEE Transactions on Software Engineering, 33(10):659--674, 2007. Google ScholarDigital Library
- G. Holzmann, R. Joshi, and A. Croce. Tackling large verification problems with the swarm tool. Proc. 15th Int'l. SPIN Workshop, 5156:134--143, 2008. Google ScholarDigital Library
- S. Khurshid, C. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. Proc. of the 9th TACAS, pages 553--568, 2003. Google ScholarDigital Library
- A. King. Distributed parallel symbolic execution. Master's thesis, Kansas State University, 2009.Google Scholar
- J. King. Symbolic execution and program testing. "Communications of the ACM", 1976. Google ScholarDigital Library
- C. Pǎsǎreanu, P. Mehlitz, D. Bushnell, K. Gundy Burlet, M. Lowry, S. Person, and M. Pape. Combining unit-level symbolic execution and system-level concrete execution for testing nasa software. In Proc. of the 2008 Int'l. Symposium on Software Testing and Analysis, pages 15--26. ACM New York, NY, USA, 2008. Google ScholarDigital Library
- C. Pǎsǎreanu, J. Schumann, P. Mehlitz, G. Karsai, H. Nine, and S. Nima. Test-case generation for Simulink / Stateflow models of software-intensive mission-critical systems. In 3rd IEEE Int'l. Conference on Space Mission Challenges for Information Technology, 2009.Google Scholar
- C. Ramamoorthy, S. Ho, and W. Chen. On the automated generation of program test data. IEEE Transactions on Software Engineering, pages 293--300, 1976. Google ScholarDigital Library
- S. Rayadurgam and M. P. Heimdahl. Coverage based test-case generation using model checkers. In Proc. of the 8th IEEE Int'l. Conference and Workshop on the Engineering of Computer Based Systems, pages 83--91. IEEE Computer Society, April 2001.Google ScholarCross Ref
- K. Sen and G. Agha. CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. Computer Aided Verification, 4144:419, 2006. Google ScholarDigital Library
- J. Siddiqui and S. Khurshid. Pkorat: Parallel generation of structurally complex test inputs. In Proc. of the 2009 International Conference on Software Testing Verification and Validation, pages 250--259. IEEE Computer Society Washington, DC, USA, 2009. Google ScholarDigital Library
- M. Staats. Towards a framework for generating tests to satisfy complex code coverage in Java Pathfinder. In Proc. of NASA Formal Methods Symposium 2009, 2009.Google Scholar
- U. Stern and D. Dill. Parallelizing the Murφ verifier. Formal Methods in System Design, 18(2):117--129, 2001. Google ScholarDigital Library
- J. Sztipanovits and G. Karsai. Generative programming for embedded systems. In Proc. of Int'l. Conference on Principles and Practice of Declarative Programming, volume 6, pages 180--180. Springer, 2002. Google ScholarDigital Library
- W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda. Model checking programs. In Proc. of Automated Software Engineering, pages 203--232. Springer, 2003. Google ScholarDigital Library
- W. Visser, C. Pǎsǎreanu, and R. Pelánek. Test input generation for java containers using state matching. In Proc. of the 2006 Int'l. Symposium on Software Testing and Analysis, pages 37--48. ACM New York, NY, USA, 2006 Google ScholarDigital Library
Index Terms
Parallel symbolic execution for structural test generation
Recommendations
Shadow Symbolic Execution with Java PathFinder
Regression testing ensures that a software system when it evolves still performs correctly and that the changes introduce no unintended side-effects. However, the creation of regression test cases that show divergent behavior needs a lot of effort. A ...
Symbolic Arrays in Symbolic PathFinder
Symbolic Execution is a program analysis technique used to increase software reliability. Modern software often manipulate complex data structures, many of which being similar to arrays. We present a novel approach and implementation in Symbolic ...
Test Case Selection Based on Path Condtions of Symbolic Execution
APSEC '12: Proceedings of the 2012 19th Asia-Pacific Software Engineering Conference - Volume 01Symbolic execution as a test case generation technique has recently become an active research area. However, since symbolic execution generates a large number of test cases, it is impractical to run all the generated test cases in practice. In this ...
Comments