Search

With the remarkable advancement of deep learning in many domains, such as in computer vision, learning-enabled systems are rapidly being adopted in safety-critical domains where it is crucial to verify and validate the system rigorously. However, due to the unique characteristics of the learning-enabled components compared to traditional systems, existing verification techniques do not work in many cases, which calls for new approaches to address this problem. In the literature, we identified that a practical and scalable testing technique is lacking for computer-vision deep neural networks (DNNs) that deal with high-dimensional and unstructured input data. Moreover, most of the existing approaches for addressing this problem are white-box solutions that are dependent on the DNN under test, solutions that may be inappropriate given the highly iterative model development workflow. To address this problem, we propose systematic testing techniques for DNNs that resolve the dependency on the model under test, since the dependency comes with several critical shortcomings. In doing so, we investigated the following three concrete ideas. First, we propose a test prioritization technique that can identify failure-revealing test inputs to help reduce the test construction cost. Second, we propose a DNN-independent test adequacy measurement technique that can measure the adequacy of testing, and also help construct a representative test suite. Third, we propose a DNN-independent test case generation technique that can synthesize realistic test cases that are effective at finding failures in the DNN under test. The last two approaches are black-box solutions in that the test adequacy measurement and the test case generation are performed independently of the DNN under test, a unique direction compared to existing approaches. The experiments showed that (1) test prioritization can effectively prioritize failure-revealing test cases, (2) the black-box coverage criterion can help construct representative test cases that achieve effectiveness comparable to those constructed with white-box criteria, but with much lower measurement cost, and (3) the black-box test generation can synthesize realistic test cases that are also effective at finding failures in the model under test. We believe that the black-box approaches bring complementary benefits to white-box approaches and that they deserve further investigation.

A common problem in automated software testing is the need to generate many inputs with complex structure in a black-box fashion. For example, a library for manipulating red-black trees may require that inputs are themselves valid red-black trees, meaning anything invalid is not suitable for testing. As another example, in order to test code generation in a compiler, it is necessary to use input programs which are both syntactically valid and well-typed. Despite the importance of this problem, we observe that existing solutions are few in number and have severe drawbacks, including unreasonably slow performance and a lack of generality to testing different systems.This thesis presents a solution to this problem of black-box structured input generation. I observe that test inputs can be described as solutions to systems of logical constraints, and that more expressive constraints can lead to more complex tests. In order to test effectively and generate many tests, we need high-performance constraint solvers capable of finding many solutions to these constraints. I observe that constraint logic programming (CLP) offers an expressive constraint language paired with a high-performance constraint solver, and thus serves as a potential solution to this problem. Via a series of case studies, I have found that CLP (1) is applicable to testing a wide variety of systems; (2) can scale to more complex constraints than ever previously described; and (3) is often orders of magnitude faster than competing solutions. These case studies have also exposed dozens of bugs in high-profile software, including the Rust compiler and the Z3 SMT solver.

Software testing is a critical stage in the life cycle of software development. The testing process costs hundreds of billions of dollars per year worldwide. Therefore, even small improvements in it could lead to very large savings. In software, testing mainly refers to dynamic testing. It involves designing and generating proper test cases for the software, executing the software with these test cases, and observing the results. The aim is to find maximum number of errors with minimum number of test cases. Black-box testing involves seeing whether the program behaves as expected. White-box testing involves knowledge of the code, to see which parts of the software were exercised during program execution. This thesis is concerned with white-box testing. The strongest form of white-box testing is path testing, in which test data is sought that leads to all different execution paths through a program being exercised. Searching for an input datum in the program's input space that meets the path coverage criterion is a search problem. Evolutionary algorithms have proven to be suitable for searching for test data. The aim of this thesis is to evaluate and improve the use of genetic algorithms (GA) for path testing. First, the capability and limitations of GA-based path testing are identified. Next we investigate possible ways to improve GA for test data generation. The obtained results are a collection of test programs; a classification scheme for test programs; understanding key GA parameters and identifying an effective default GA parameter setup; understanding the effects of infeasible paths; a model that stops GA searching when it seems ineffective to keep going, saving time while still finding almost all feasible paths; and identifying an effective hybrid of GA and local search techniques. The results have the following implications: • The collection of test programs can serve as a testing benchmark for proposed software testing approaches. • The classification of test programs provides ways to group test programs with similar characteristics. • The key parameters are shown in order to be population size, allele range, and number of generations. Suitable default values for these parameters are identified, which can represent a common setup to be used with an unknown new test program. • The existence of infeasible paths is shown not to hinder the process of test data generation, rather it improves the performance by encouraging diversity in the population. This means that the costly task of analyzing target paths to identify and remove infeasible ones is not necessary. • The proposed stopping criteria can stop searching whenever it is not worth continuing because the likelihood of finding further paths is too low. It is shown to be effective in stopping searching quite early, while missing almost no feasible paths. One less arbitrary system parameter (maximum number of generations to search) can be removed as a result. • The hybrid GAs improve the performance both in terms of path coverage and number of generations required for the search.