Sasa Misailovic
ABSTRACT
We present novel algorithms for parallel testing of code that takes structurally complex test inputs. The algorithms build on the Korat algorithm for constraint-based generation of structurally complex test inputs. Given an imperative predicate that specifies the desired structural constraints and a finitization that bounds the desired input size, Korat performs a systematic search to generate all test inputs (within the bounds) that satisfy the constraints. We present how to generate test inputs with a parallel search in Korat and how to execute test inputs in parallel, both off-line (when the inputs are saved on disk) and on-line (when execution immediately follows generation).
The inputs that Korat generates enable bounded-exhaustive testing that checks the code under test exhaustively for all inputs within the given bounds. We also describe a novel methodology for reducing the number of equivalent inputs that Korat can generate. Our development of parallel Korat and the methodology for reducing equivalent inputs are motivated by testing an application developed at Google. The experimental results on running parallel Korat across up to 1024 machines on the Google's infrastructure show that parallel test generation and execution can achieve significant speedup, up to 543.55 times.
- F. A. Aloul, A. Ramani, I. L. Markov, and K. A. Sakallah. Solving difficult SAT instances in the presence of symmetry. In Proc. of the 39th Conference on Design Automation, 2002. Google Scholar
Digital Library
- J. Barnat, L. Brim, and J. Chaloupka. Parallel breadth-first search ltl model-checking. In Proc. of the 18th IEEE International Conference on Automated Software Engineering, 2003.Google ScholarDigital Library
- B. Beizer. Software Testing Techniques. International Thomson Computer Press, 1990. Google ScholarDigital Library
- C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on Java predicates. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA), July 2002. Google ScholarDigital Library
- L. A. Clarke. A system to generate test data and symbolically execute programs. IEEE Transactions on Software Engineering, Sept. 1976. Google ScholarDigital Library
- J. Crawford, M. Ginsberg, E. Luks, and A. Roy. Symmetry-breaking predicates for search problems. In Proc. Fifth International Conference on Principles of Knowledge Representation and Reasoning, 1996.Google ScholarDigital Library
- J. Dean and S. Ghemawat. MapReduce: Simplified data processing on large clusters. In Sixth Symposium on Operating System Design and Implementation, San Francisco, CA, Dec. 2004. Google ScholarDigital Library
- M. B. Dwyer, S. Elbaum, S. Person, and R. Purandare. Parallel randomized state-space search. In Proc. of the 29th International Conference on Software Engineering (ICSE), Minneapolis, MN, May 2007. Google ScholarDigital Library
- S. Ghemawat, H. Gobioff, and S. Leung. The Google file system. In 19th Symposium on Operating Systems Principles, Lake George, NY, 2003. Google ScholarDigital Library
- A. Gotlieb, B. Botella, and M. Rueher. Automatic test data generation using constraint solving techniques. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA), Clearwater Beach, FL, 1998. Google ScholarDigital Library
- A. Grama and V. Kumar. State of the art in parallel search techniques for discrete optimization problems. IEEE Trans. Knowl. Data Eng., 11(1):28--35, 1999. Google ScholarDigital Library
- G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), May 1997. Google ScholarDigital Library
- J. C. Huang. An approach to program testing. ACM Computing Surveys, 7(3), 1975. Google ScholarDigital Library
- R. Iosif. Exploiting heap symmetries in explicit-state model checking of software. In Proc. of the 16th Conference on Automated Software Engineering (ASE), Nov. 2001. Google ScholarDigital Library
- D. Jackson. Software Abstractions: Logic, Language and Analysis. The MIT Press, Cambridge, MA, 2006. Google ScholarDigital Library
- V. K. Janakiram, D. P. Agrawal, and R. Mehrotra. A randomized parallel backtracking algorithm. IEEE Trans. Comput., 37(12):1665--1676, 1988. Google ScholarDigital Library
- M. D. Jones and J. Sorber. Parallel search for ltl violations. Int. J. Softw. Tools Technol. Transf., 7(1):31--42, 2005.Google ScholarDigital Library
- R. M. Karp and Y. Zhang. Randomized parallel algorithms for backtrack search and branch-and-bound computation. J. ACM, 40(3):765--789, 1993. Google ScholarDigital Library
- S. Khurshid. Generating Structurally Complex Tests from Declarative Constraints. PhD thesis, Dept. of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, 2003. Google ScholarDigital Library
- S. Khurshid and D. Marinov. Checking Java implementation of a naming architecture using TestEra. In S. D. Stoller and W. Visser, editors, Electronic Notes in Theoretical Computer Science (ENTCS), volume 55. Elsevier Science Publishers, 2001.Google Scholar
- S. Khurshid and D. Marinov. TestEra: Specification-based testing of Java programs using SAT. Automated Software Engineering Journal, 11(4):403--434, Oct. 2004. Google ScholarDigital Library
- S. Khurshid, D. Marinov, I. Shlyakhter, and D. Jackson. A case for efficient solution enumeration. In Proc. of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), Santa Margherita Ligure, Italy, May 2003.Google Scholar
- J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7), 1976. Google ScholarDigital Library
- B. Korel. Automated test data generation for programs with procedures. In Proc. of the International Symposium on Software Testing and Analysis, San Diego, CA, 1996. Google ScholarDigital Library
- R. Kumar and E. G. Mercer. Load balancing parallel explicit state model checking. Electr. Notes Theor. Comput. Sci., 128(3):19--34, 2005.Google ScholarDigital Library
- F. Lerda and R. Sisto. Distributed-memory model checking with spin. In Proc. of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, pages 22--39, 1999. Google ScholarDigital Library
- F. Lerda and W. Visser. Addressing dynamic issues of program model checking. Lecture Notes in Computer Science, 2057:80--102, 2001. Google ScholarDigital Library
- B. Liskov and J. Guttag. Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, 2000. Google ScholarDigital Library
- D. Marinov. Automatic Testing of Software with Structurally Complex Inputs. PhD thesis, Dept. of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, 2004. Google ScholarDigital Library
- D. Marinov, A. Andoni, D. Daniliuc, S. Khurshid, and M. Rinard. An evaluation of exhaustive testing for data structures. Technical Report MIT-LCS-TR-921, MIT Computer Science and Artificial Intelligence Lab, Cambridge, MA, Sept. 2003.Google Scholar
- B. D. McKay. Practical graph isomorphism. Congressus Numerantium, 1(30):45--87, 1981. http://cs.anu.edu.au/~bdm/nauty/.Google Scholar
- W. M. McKeeman. Differential testing for software. Digital Technical Journal, 10(1), 1998.Google Scholar
- A. Milicevic, S. Misailovic, D. Marinov, and S. Khurshid. Korat: A tool for generating structurally complex test inputs. In Proc. of the International Conference on Software Engineering, Demo Papers (ICSE Demo 2007), pages 771--774, Minneapolis, MN, May 2007. Google ScholarDigital Library
- S. Misailovic, A. Milicevic, S. Khurshid, and D. Marinov. Generating test inputs for fault-tree analyzers using imperative predicates. In the Workshop on Advances and Innovations in Systems Testing (STEP 2007), Memphis, TN, May 2007.Google Scholar
- R. Palmer and G. Gopalakrishnan. A distributed partial order reduction algorithm. In FORTE '02: Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, pages 370--379, 2002. Google ScholarDigital Library
- C. V. Ramamoorthy, S.-B. F. Ho, and W. T. Chen. On the automated generation of program test data. IEEE Transactions on Software Engineering, 2(4), 1976. Google ScholarDigital Library
- N. J. A. Sloane, S. Plouffe, J. M. Borwein, and R. M. Corless. The encyclopedia of integer sequences. SIAM Review, 38(2), 1996. http://www.research.att.com/~njas/sequences/Seis.html.Google Scholar
- U. Stern and D. L. Dill. Parallelizing the murphi verifier. In CAV '97: Proceedings of the 9th International Conference on Computer Aided Verification, pages 256--278, London, UK, 1997. Springer-Verlag. Google ScholarDigital Library
- U. Stern and D. L. Dill. Parallelizing the Muro verifier. Formal Methods in System Design, 2001. Google ScholarDigital Library
- K. Stobie. Advanced modeling, model based test generation, and Abstract state machine Language (AsmL). Seattle Area Software Quality Assurance Group, http://www.sasqag.org/pastmeetings/asml.ppt, Jan. 2003.Google Scholar
- K. Sullivan, J. Yang, D. Coppit, S. Khurshid, and D. Jackson. Software assurance by bounded exhaustive testing. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA), 2004. Google ScholarDigital Library
- R. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146--160, 1972.Google ScholarDigital Library
- M. Veanes, C. Campbell, W. Schulte, and N. Tillmann. Online testing with model programs. In Proceedings of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 273--282, New York, NY, 2005. ACM Press. Google ScholarDigital Library
- W. Visser, K. Havelund, G. Brat, and S. Park. Model checking programs. In Proc. of the 15th Conference on Automated Software Engineering (ASE), Grenoble, France, 2000. Google ScholarDigital Library
- E. J. Weyuker and T. J. Ostrand. Theories of program testing and the application of revealing subdomains. IEEE Transactions on Software Engineering, 6(3), May 1980. Google ScholarDigital Library
- T. Xie, D. Marinov, and D. Notkin. Rostra: A framework for detecting redundant object-oriented unit tests. In Proc. of the 19th IEEE International Conference on Automated Software Engineering, Sept. 2004. Google ScholarDigital Library
Index Terms
- Parallel test generation and execution with Korat
Recommendations
Parallel Test Prioritization
Although regression testing is important to guarantee the software quality in software evolution, it suffers from the widely known cost problem. To address this problem, existing researchers made dedicated efforts on test prioritization, which optimizes ...
Korat: automated testing based on Java predicates
This paper presents Korat, a novel framework for automated testing of Java programs. Given a formal specification for a method, Korat uses the method precondition to automatically generate all (nonisomorphic) test cases up to a given small size. Korat ...
Optimizing parallel Korat using invalid ranges
SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of SoftwareConstraint-based input generation enables systematic testing for effective bug finding, but requires exploration of very large spaces of candidate inputs. This paper introduces a novel approach to optimize input generation using Korat – a solver for ...
Comments