Browsing by Subject "Test input generation"
Now showing 1 - 4 of 4
Results Per Page
Sort Options
Item Contract-driven data structure repair : a novel approach for error recovery(2014-05) Nokhbeh Zaeem, Razieh; Khurshid, SarfrazSoftware systems are now pervasive throughout our world. The reliability of these systems is an urgent necessity. A large degree of research effort on increasing software reliability is dedicated to requirements, architecture, design, implementation and testing---activities that are performed before system deployment. While such approaches have become substantially more advanced, software remains buggy and failures remain expensive. We take a radically different approach to reliability from previous approaches, namely contract-driven data structure repair for runtime error recovery, where erroneous executions of deployed software are corrected on-the-fly using rich behavioral contracts. Our key insight is to transform the software contract---which gives a high level description of the expected behavior---to an efficient implementation which repairs the erroneous data structures in the program state upon an error. To improve efficiency, scalability, and effectiveness of repair, in addition to rich behavioral contracts, we leverage the current erroneous state, dynamic behavior of the program, as well as repair history and abstraction. A core technical problem our approach to repair addresses is construction of structurally complex data that satisfy desired properties. We present a novel structure generation technique based on dynamic programming---a classic optimization approach---to utilize the recursive nature of the structures. We use our technique for constraint-based testing. It provides better scalability than previous work. We applied it to test widely-used web browsers and found some known and unknown bugs. Our use of dynamic programming in structure generation opens a new future direction to tackle the scalability problem of data structure repair. This research advances our ability to develop correct programs. For programs that already have contracts, error recovery using our approach can come at a low cost. The same contracts can be used for systematically testing code before deployment using existing as well as our new techniques. Thus, we enable a novel unification of software verification and error recovery.Item Improving constraint-based test input generation using Korat(2015-05) Srinivasan, Raghavendra; Khurshid, SarfrazKorat is an existing technique for test input generation using imperative constraints that describe properties of desired inputs written as Java predicates, termed RepOk methods, which are executable checks for those properties. Korat efficiently prunes the space of candidate inputs for the RepOk method by executing it on candidate inputs and monitoring the object fields that RepOk accesses in deciding if the properties are satisfied. While Korat generates inputs effectively, its correctness and efficiency rely on two assumptions about the RepOk methods. For correctness, Korat assumes the RepOk methods do not use the Java reflection API for field accesses; the use of reflection renders Korat unable to enumerate all desired inputs. For efficiency, Korat assumes the RepOk methods do not make unnecessary field accesses, which can reduce the effectiveness of Korat’s pruning. Our thesis addresses both these limitations. To support reflection, we build on the core Korat to enhance it such that it can monitor field accesses based on reflection. To assist the users with writing RepOk’s, we introduce a static analysis tool that detects potential places where the input RepOk may be edited to enhance performance of Korat. We also present experimental results using a suite of standard data structure subjects.Item Improving dynamic analysis with data flow analysis(2010-08) Chang, Walter Chochen; Lin, Yun Calvin; McKinley, Kathryn; Browne, James C.; Khurshid, Sarfraz; Myers, AndrewMany challenges in software quality can be tackled with dynamic analysis. However, these techniques are often limited in their efficiency or scalability as they are often applied uniformly to an entire program. In this thesis, we show that dynamic program analysis can be made significantly more efficient and scalable by first performing a static data flow analysis so that the dynamic analysis can be selectively applied only to important parts of the program. We apply this general principle to the design and implementation of two different systems, one for runtime security policy enforcement and the other for software test input generation. For runtime security policy enforcement, we enforce user-defined policies using a dynamic data flow analysis that is more general and flexible than previous systems. Our system uses the user-defined policy to drive a static data flow analysis that identifies and instruments only the statements that may be involved in a security vulnerability, often eliminating the need to track most objects and greatly reducing the overhead. For taint analysis on a set of five server programs, the slowdown is only 0.65%, two orders of magnitude lower than previous taint tracking systems. Our system also has negligible overhead on file disclosure vulnerabilities, a problem that taint tracking cannot handle. For software test case generation, we introduce the idea of targeted testing, which focuses testing effort on select parts of the program instead of treating all program paths equally. Our “Bullseye” system uses a static analysis performed with respect to user-defined “interesting points” to steer the search down certain paths, thereby finding bugs faster. We also introduce a compiler transformation that allows symbolic execution to automatically perform boundary condition testing, revealing bugs that could be missed even if the correct path is tested. For our set of 9 benchmarks, Bullseye finds bugs an average of 2.5× faster than a conventional depth-first search and finds numerous bugs that DFS could not. In addition, our automated boundary condition testing transformation allows both Bullseye and depth-first search to find numerous bugs that they could not find before, even when all paths were explored.Item MKorat : a novel approach for memorizing the Korat search and some potential applications(2016-05) Dini, Nima; Khurshid, Sarfraz; Gligoric, MilosWriting logical constraints that describe properties of desired inputs enables an effective approach for systematic software testing, which can find many bugs. The key problem in systematic constraint-based testing is efficiently exploring very large spaces of all possible inputs to enumerate desired valid inputs. The Korat technique provides an effective solution to this problem. Korat uses desired input properties written as imperative predicates and implements a backtracking search that prunes large parts of the input space and enumerates all non-isomorphic inputs within a given bound on input size. Despite the effectiveness of Korat’s pruning, systematically creating and running large numbers of tests can be costly in practice. Previous work introduced parallel test generation and execution using Korat to make it more practical. We build on a specific algorithm, SEQ-ON, introduced in previous work for equi-distancing candidate inputs, which allows re-execution of Korat for input generation using parallel workers with evenly distributed workload. Our key insight is that the Korat search typically encounters many consecutive candidates that are all invalid inputs and such invalid ranges of candidates can be memoized succinctly to optimize re-execution of Korat. We introduce a novel approach for memoizing Korat’s checking of consecutive invalid candidates, embody the approach into three new techniques based on SEQ-ON, evaluate the techniques using a standard suite of data structure subjects to show the efficacy of our approach, and show some potential applications of it in two new application domains for Korat. We believe our work opens a promising new direction to optimize solving of imperative constraints and using them in novel application domains.