We present a novel technique for producing bounded exhaustive test suites from hybrid invariants, i.e., invariants that are expressed imperatively, declaratively, or as a combination of declarative and imperative predicates. Hybrid specifications are processed using known mechanisms for the imperative and declarative parts, but combined in a way that enables us to exploit information from the declarative side, such as tight bounds computed from the declarative specification, to improve the search both on the imperative and declarative sides. Moreover, our technique automatically evaluates different possible ways of processing the imperative side, and the alternative settings (imperative or declarative) for parts of the invariant available both declaratively and imperatively, to decide the most convenient invariant configuration with respect to efficiency in test generation. This is achieved by transcoping, i.e., by assessing the efficiency of the different alternatives on small scopes (where generation times are negligible), and then extrapolating the results to larger scopes.

We describe an automated approach for systematic black-box testing of database management systems (DBMS) using a relational constraint solver. We reduce the problem of automated database testing into generating three artifacts: (1) SQL queries for testing, (2) meaningful input data to populate test databases, and (3) expected results of executing the queries on the generated data. We leverage our previous work on ADUSA and the Automated SQL Query Generator to form high-quality test suites for testing DBMS engines. This paper presents a detailed description of our framework for Automated SQL Query Generation using the Alloy tool-set, and experimental results of testing database engines using our framework. We show how the main SQL grammar constraints can be solved by translating them to Alloy constraints to generate semantically and syntactically correct SQL queries. We also present experimental results of combining ADUSA and the Automated SQL Query Generator, and applying our framework to test the Oracle 11g database. Our framework generated 5 new queries, which reveal erroneous behavior of Oracle 11g.

The last decade has seen many advances in test input generation, specifically using systematic approaches that can enumerate many tests. While such approaches have enhanced our ability to find bugs in programs, running large numbers of tests remains a time consuming and expensive task, especially for tests that execute operations on external resources, such as a file system or a network. This paper presents a novel technique for optimizing execution of suites of tests, where several tests in a suite may contain common initial execution -- a property often exhibited by systematically generated suites, e.g., those for bounded exhaustive testing. Our insight is that we can cluster execution of such tests by defining abstract-level undo operations, which allow a common execution segment to be performed once, and its result to be shared across the tests, which then perform the rest of their operations. We present our framework for clustered execution of test suites, and evaluate it using three case-studies, which show our technique enables significant performance speed-up over traditional test execution.

The use of specifications provides an effective technique to automate testing. A form of specification that automates generation of test inputs is logical constraints that define properties of desired inputs. Recent advances in constraint solving technology have made the use of constraints particularly attractive. However, manually writing constraints to define complex inputs to real-world programs can pose a significant burden on the user and restrict their wider use. We envision a novel approach to facilitate the use of constraints: to provide a mixed notation for writing the properties. Our key insight is that different properties can lend to easier formulation using different programming paradigms. Thus, a notation that supports more than one paradigm, e.g., declarative and imperative paradigms, can enable achieving a sweet-spot in minimizing the manual effort required in constraint formulation. Moreover, solving such constraints is also likely to be more efficient as different properties may require different paradigms for more direct and accurate representation. This paper presents our vision and gives an illustration to make a case for the usefulness of such a notation.

This tool paper presents an embodiment of TestEra - a framework developed in previous work for specification-based testing of Java programs. To test a Java method, TestEra uses the method's pre-condition specification to generate test inputs and the post-condition to check correctness of outputs. TestEra supports specifications written in Alloy - a first-order, declarative language based on relations - and uses the SAT-based back-end of the Alloy tool-set for systematic generation of test suites. Each test case is a JUnit test method, which performs three key steps: (1) initialization of pre-state, i.e., creation of inputs to the method under test; (2) invocation of the method; and (3) checking the correctness of post-state, i.e., checking the method output. The tool supports visualization of inputs and outputs as object graphs for graphical illustration of method behavior. TestEra is available for download to be used as a library or as an Eclipse plug-in.

We present a novel approach for generating syntactically and semantically correct SQL queries as inputs for testing relational databases. We leverage the SAT-based Alloy tool-set to reduce the problem of generating valid SQL queries into a SAT problem. Our approach translates SQL query constraints into Alloy models, which enable it to generate valid queries that cannot be automatically generated using conventional grammar-based generators.

We present a novel approach for black-box testing of database management systems (DBMS) using the Alloy tool-set. Given a database schema and an SQL query as inputs, our approach first formulates Alloy models for both inputs, and then using the Alloy Analyzer, it generates (1) input data to populate test databases, and (2) the expected result of executing the given query on the generated data. The Alloy Analyzer results form a complete test suite (input/oracle) for verifying the execution result of a DBMS query processor. By incorporating both the schema and the query during the analysis, our approach performs query-aware data generation where executing the query on the generated data produces meaningful non-empty results. We developed a prototype tool, ADUSA, and used it to evaluate our approach. Experimental results show the ability of our approach to detect bugs in both open-source as well as commercial database management systems.