Browsing by Subject "Korat"
Now showing 1 - 7 of 7
- Results Per Page
- Sort Options
Item A visualization tool for recursive linked structures generated by Korat(2018-04-26) Ren, Yuanrui; Khurshid, SarfrazThis report presents Korat-Viz, an off-line visualization tool for Korat, a framework for generating test cases of Java programs. Given a predicate specifying the structural properties and a bound on the desired test input size, Korat can generate all test cases satisfying these two requirements. The default representation of the generated test cases in Korat is candidate vector. Korat-Viz provides a graphical representation of the test cases, helping users to have a better understanding of the Korat search and the generated test cases. More specifically, our implementation focuses on recursive linked data structures, such as linked lists and binary trees, which are commonly used in Java libraries and are standard examples for the Korat tool.Item Backward-Korat : improving Korat search to enable backward input space exploration(2017-05-03) Yelen, Cagdas; Khurshid, Sarfraz; Julien, Christine L.Automated test input generation plays an important role in increasing software quality. Exhaustively testing a program for all test inputs within a given bound helps check many corner cases that are easy to miss otherwise. Korat is a constraint solver and an automated testing framework for bounded exhaustive testing of Java programs. Korat uses a predicate method that describes desired inputs and a finitization bound to explore the space of all candidate inputs and generates the desired ones. Korat performs a systematic backtracking search for input space exploration based on pruning and isomorphism breaking. The Korat search gains part of its efficiency by monitoring executions of the given predicate on candidate inputs and creating new candidates based on the object fields accessed by the predicate during its execution. The Korat search has a default order for exploring the candidate inputs -- the search always performs the same exploration for the same predicate and finitization. Our thesis is that a different search order for the Korat search can enhance the efficacy of Korat. Specifically, we introduce the backward Korat, a novel approach to enable Korat to go backward in the search space. Our technique is built on the core of the traditional Korat search. The backward Korat can be applied to a variety of existing techniques including constraint-based data structure repair, parallel Korat, etc. We evaluate our approach using a standard suite of data structures. The experimental results show that the backward search works well and generates the same test inputs as the traditional search produces even though it performs slower compared to the forward search. Using the backward search and the traditional Korat search in tandem enables a new set of possible applications.Item Constraint prioritization for efficient test generation using Korat(2007-12) Kulkarni, Amresh Vishveshvar; Khurshid, SarfrazA key problem in software testing is generating a set of test cases which check for a variety of behaviors of a given software system. For testing programs that take inputs that are structurally complex it is imperative to come up with a way to increase efficiency for generating these complex structures. We take an existing algorithm for test case generation, Korat, and show how to improve its performance using constraint prioritization. The technique used in Korat is to perform bounded exhaustive testing using state space exploration to generate non-isomorphic structures. Korat uses a predicate method written by user which defines constraints for the desired data structure. We describe a technique for re-writing the predicate method to enable Korat to generate tests more efficiently.Item Efficient state space exploration for parallel test generation(2009-05) Ramasamy Kandasamy, Manimozhian; Khurshid, Sarfraz; Perry, Dewayne E.Automating the generation of test cases for software is an active area of research. Specification based test generation is an approach in which a formal representation of a method is analyzed to generate valid test cases. Constraint solving and state space exploration are important aspects of the specification based test generation. One problem with specification based testing is that the size of the state space explodes when we apply this approach to a code of practical size. Hence finding ways to reduce the number of candidates to explore within the state space is important to make this approach practical in industry. Korat is a tool which generates test cases for Java programs based on predicates that validate the inputs to the method. Various ongoing researches intend to increase the tools effectiveness in handling large state space. Parallelizing Korat and minimizing the exploration of invalid candidates are the active research directions. This report surveys the basic algorithms of Korat, PKorat, and Fast Korat. PKorat is a parallel version of Korat and aims to take advantage of multi-processor and multicore systems available. Fast Korat implements four optimizations which reduce the number of candidate explored to generate validate candidates and reduce the amount of time required to explore each candidate. This report also presents the execution time results for generating test candidates for binary tree, doubly linked list, and sorted singly linked list, from their respective predicates.Item Enhancing usability and applicability of Korat(2015-08) Bhaskar, Kilnagar S.; Khurshid, Sarfraz; Krasner, HerbSoftware testing is an integral part of the software development cycle, and involves various techniques to test software components and applications. Specification-based testing focuses on expected functionality as described in given specifications. Korat is a tool for generating structurally complex test inputs for specification-based testing of Java programs that operate on such inputs. Korat uses specifications written as Java predicates, that describe properties of expected input structures and efficiently generates all non-isomorphic valid structures within given bounds on input size. This report describes the software requirements, application design and implementation details of our effort to improve usability and applicability of Korat. Our work involves functional enhancements to the classic Korat tool to provide support for the following elements: Graphical User Interface (GUI), Java Universal Network/Graph Framework (JUNG) output, Finite State Machine Domain (FSM), and JavaScript Object Notation (JSON) graph archival.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 Pairwise-Korat : automated testing using Korat in an industrial setting(2015-05) Zhong, Hua, M.S.in Engineering; Khurshid, Sarfraz; Zhang, LingmingIn this report, we present an algorithm for testing applications which takes structurally complex test inputs. The algorithm, Pairwise-Korat, adopts Korat -- an algorithm for constraint-based generation of structurally complex test inputs. Korat takes (1) an imperative predicate which specifies the desired structural integrity constraints and (2) a finitization which bounds the desired test inputs size. Korat performs a systematic search to generate all test inputs (within the bounds) for which the predicate returns true. We present how to generate test inputs in Korat and how to execute test inputs in parallel. The inputs that Korat generates enable bounded-exhaustive testing that checks the code under test exhaustively for all inputs within the given bounds. We also describe a novel methodology for reducing the number of equivalent inputs that Korat generates. Our development of test input generation and the methodology for reducing equivalent inputs are motivated by testing applications developed at eBay. The experimental results show that the Pairwise-Korat achieves great performance in finding defects and increasing test coverage and the algorithm outperforms current manual solutions adopted at the company.