Automatic Test Case Generation
Manual software testing, in general, and test case generation, in particular, are labor-intensive processes. Automated testing can significantly reduce the cost of software development and maintenance. To automate testing of Java programs, we explore systematic generation of test cases from models of program inputs given as first-order relational formulas in the Alloy Modelling Language.
Properties of Alloy models can be automatically analyzed using the Alloy Analyzer, which finds satisfying assignments for relational formulas by translating the formulas into boolean satisfiability formulas and using off-the-shelf SAT solvers. A satisfying assignment for a formula that relates values of program variables at a control point is simply an assignment of values to these variables such that the formula evaluates to true. Thus, for a formula that expresses a method precondition, a satisfying assignment corresponds to a valid input for the method. This observation forms the basis of the TestEra tool. TestEra implements a novel approach for automatic test case generation: (1) given a method precondition as a formula, generate all nonisomorphic satisfying assignments (within a given bound); (2) concretize these assignments to generate method inputs and execute the method on each input; (3) abstract the method's outputs and verify the correctness of each input/output pair by evaluating a formula that represents the method postcondition.
For more information, visit the MulSaw project page, the MulSaw homepage, or email khurshid@lcs.mit.edu.
Members
Publications
- Sarfraz Khurshid, Darko Marinov, Ilya Shlyakhter and Daniel Jackson. A Case for Efficient Solution Enumeration. 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), Portofino, Italy. May 2003. (To appear.) (PDF)
- Sarfraz Khurshid and Darko Marinov. TestEra: A Novel
Framework for Automated Testing of Java Programs. Invited
submission to Automated Software Engineering Journal,
December 2002. (PDF)
[A previous version appeared at the 16th IEEE International Conference on Automated Software Engineering (ASE 2001) and was nominated for the best paper award by the program committee. (PDF)] - Sarfraz Khurshid, Darko Marinov, Checking Java Implementation of a Naming Architecture Using TestEra. CAV Workshop on Software Model Checking. Electronic Notes in Theoretical Computer Science (ENTCS 55(3)), July 2001. (PDF)
- Sarfraz Khurshid and Darko Marinov. Using TestEra to Check the Intentional Naming System of Oxygen (Extended Abstract).MIT Student Oxygen Workshop, Gloucester, MA. July 2001. (PDF)
Related Publications
- Sarfraz Khurshid, Corina Pasareanu and Willem Visser. Generalized Symbolic Execution for Model Checking and Testing. 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2003), Warsaw, Poland. April 2003. (To appear.) (PDF)
- Sarfraz Khurshid, Darko Marinov and Daniel Jackson. An Analyzable Annotation Language. 17th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2002), Seattle, WA. November 2002. (PDF)
- Alexandr Andoni, Dumitru Daniliuc, Sarfraz Khurshid, and Darko Marinov. Evaluating the "Small Scope Hypothesis". (Submitted for publication.) September 2002. (PS)
- Chandrasekhar Boyapati, Sarfraz Khurshid and Darko Marinov. Korat: Automated Testing Based on Java Predicates. ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2002), Rome, Italy. July 2002. (This paper won an ACM SIGSOFT Distinguished Paper Award) (PDF)
- Darko Marinov and Sarfraz Khurshid. VAlloy: Virtual Functions Meet a Relational Language. 11th International Symposium of Formal Methods Europe (FME 2002), Copenhagen, Denmark. July 2002. (PDF)
- Patrice Godefroid and Sarfraz Khurshid. Exploring Very Large State Spaces Using Genetic Algorithms. 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2002), Grenoble, France. April 2002. (Pre-selected for a special issues of the Software Tools and Technology Transfer Journal.) (PDF)
- Sarfraz Khurshid. Testing an Intentional Naming Scheme Using Genetic Algorithms. 7th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2001), Genova, Italy. April 2001. (PDF)