Generating structurally complex tests from declarative constraints

This dissertation describes a method for systematic constraint-based test generation for programs that take as inputs structurally complex data, presents an automated SAT-based framework for testing such programs, and provides evidence on the feasibility of using this approach to generate high quality test suites and find bugs in non-trivial programs. The framework tests a program systematically on all nonisomorphic inputs (within a given bound on the input size). Test inputs are automatically generated from a given input constraint that characterizes allowed program inputs. In unit testing of object-oriented programs, for example, an input constraint corresponds to the representation invariant; the test inputs are then objects on which to invoke a method under test. Input constraints may additionally describe test purposes and test selection criteria. Constraints are expressed in a simple (first-order) relational logic and solved by translating them into propositional formulas that are handed to an off-the-shelf SAT solver. Solutions found by the SAT solver are lifted back to the relational domain and reified as tests. The TestEra tool implements this framework for testing Java programs. Ex-periments on generating several complex structures indicate the feasibility of using off-the-shelf SAT solvers for systematic generation of nonisomorphic structures. The tool also uncovered previously unknown errors in several applications including an intentional naming scheme for dynamic networks and a fault-tree analysis system developed for NASA.

Department dc:contributor.department

Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2004

Author dc:creator

• Khurshid, Sarfraz, 1972-

Advisor dc:contributor.advisor

• Daniel Jackson.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/30083

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/30083