Browsing by Subject "Coverage"
Now showing 1 - 5 of 5
Results Per Page
Sort Options
Item AUnit - a testing framework for alloy(2014-05) Sullivan, Allison; Khurshid, SarfrazWriting declarative models of software designs and analyzing them to detect defects is an effective methodology for developing more dependable software systems. However, writing such models correctly can be challenging for practitioners who may not be proficient in declarative programming, and their models themselves may be buggy. We introduce the foundations of a novel test automation framework, AUnit, which we envision for testing declarative models written in Alloy -- a first-order, relational language that is supported by its SAT-based analyzer. We take inspiration from the success of the family of xUnit frameworks that are used widely in practice for test automation, albeit for imperative or object-oriented programs. The key novelty of our work is to define a basis for unit testing for Alloy, specifically, to define the concepts of test case and test coverage as well as coverage criteria for declarative models. We reduce the problems of declarative test execution and coverage computation to partial evaluation without requiring SAT solving. Our vision is to blend how developers write unit tests in commonly used programming languages with how Alloy users formulate their models in Alloy, thereby facilitating the development and testing of Alloy models for both new Alloy users as well as experts. We illustrate our ideas using a small but complex Alloy model. While we focus on Alloy, our ideas generalize to other declarative languages (such as Z, B, ASM).Item Control flow graph visualization and its application to coverage and fault localization in Python(2015-05) Salling, Jackson Lee; Khurshid, Sarfraz; Julien, ChristineThis report presents a software testing tool that creates visualizations of the Control Flow Graph (CFG) from Python source code. The CFG is a representation of a program that shows execution paths that may be taken by the machine. Similar techniques to the ones here could be applied to many other languages, but the CFGs in this tool are tailored to the Python language. As computers get faster, tools to help programmers be effective at work can become more complex and still give quick feedback, without causing an undue performance burden. This tool explores several approaches to giving feedback to developers through a visualization of the CFG. First, just the viewing of a CFG gives a different perspective on the code. A programmer could choose to juxtapose the CFG with complexity metrics during development, seeing increased complexity as graphs grow larger. Second, the tool implements a mechanism to provide code coverage to Python modules. This feature extends the visualization to show code coverage as a highlighted CFG. Test coverage requirements are calculated to check node, edge, edge-pair, and prime path coverage. From studying existing testing tools, it appears no existing tool for Python provides all these test coverage levels. Third, the tool provides an interface for adding custom highlighting of the CFG, used here to visualize fault localization. Seeing the most suspicious locations from fault localization techniques could be used to reduce debugging time. The results of running the tool on several popular Python packages, and on itself, show its performance is competitive with the most popular coverage tool when measuring branch coverage. It is slightly slower on statement cover- age alone, but much faster against an unoptimized version and a logic coverage tool. This report also presents ideas for extensions to the tool. Among them is to incorporate program repair using fault localization and mutation operators. Visualizing code as a CFG provides interesting ways to look at many software testing metrics.Item Fast error detection with coverage guarantees for concurrent software(2013-05) Coons, Katherine Elizabeth; McKinley, Kathryn S.Concurrency errors are notoriously difficult to debug because they may occur only under unexpected thread interleavings that are difficult to identify and reproduce. These errors are increasingly important as recent hardware trends compel developers to write more concurrent software and to provide more concurrent abstractions. This thesis presents algorithms that dynamically and systematically explore a program's thread interleavings to manifest concurrency bugs quickly and reproducibly, and to provide precise incremental coverage guarantees. Dynamic concurrency testing tools should provide (1) fast response -- bugs should manifest quickly if they exist, (2) reproducibility -- bugs should be easy to reproduce and (3) coverage -- precise correctness guarantees when no bugs manifest. In practice, most tools provide either fast response or coverage, but not both. These goals conflict because a program's thread interleavings exhibit exponential state- space explosion, which inhibits fast response. Two approaches from prior work alleviate state-space explosion. (1) Partial-order reduction provides full coverage by exploring only one interleaving of independent transitions. (2) Bounded search provides bounded coverage by enumerating only interleavings that do not exceed a bound. Bounded search can additionally provide guarantees for cyclic state spaces for which dynamic partial-order reduction provides no guarantees. Without partial-order reduction, however, bounded search wastes most of its time exploring executions that reorder only independent transitions. Fast response with coverage guarantees requires both approaches, but prior work failed to combine them soundly. We combine bounded search with partial-order reduction and extensively analyze the space of dynamic, bounded partial-order reduction strategies. First, we prioritize with a best-first search and show that heuristics that combine these approaches find bugs quickly. Second, we restrict partial-order reduction to combine approaches while maintaining bounded coverage. We specialize this approach for several bound functions, prove that these algorithms guarantee bounded coverage, and leverage dynamic information to further reduce the state space. Finally, we bound the partial order on a program's transitions, rather than the total order on those transitions, to combine these approaches without sacrificing partial-order reduction. This algorithm provides fast response, incremental coverage guarantees, and reproducibility. We manifest bugs an order of magnitude more quickly than previous approaches and guarantee incremental coverage in minutes or hours rather than weeks, helping developers find and reproduce concurrency errors. This thesis makes bounded stateless model checking for concurrent programs substantially more efficient and practical.Item Flower constellation optimization and implementation(2009-05-15) Bruccoleri, ChristianSatellite constellations provide the infrastructure to implement some of the most important global services of our times both in civilian and military applications, ranging from telecommunications to global positioning, and to observation systems. Flower Constellations constitute a set of satellite constellations characterized by periodic dynamics. They have been introduced while trying to augment the existing design methodologies for satellite constellations. The dynamics of a Flower Constellation identify a set of implicit rotating reference frames on which the satellites follow the same closed-loop relative trajectory. In particular, when one of these rotating reference frames is ?Planet Centered, Planet Fixed?, then all the orbits become compatible (or resonant) with the planet; consequently, the projection of the relative path on the planet results in a repeating ground track. The satellite constellations design methodology currently most utilized is the Walker Delta Pattern or, more generally, Walker Constellations. The set of orbital planes and initial spacecraft positions are represented by a set of only three integers and two real parameters rather than by all the orbital elements; Flower Constellations provide a more general framework in which most of the former restrictions are removed, by allowing the use of resonant elliptical orbits. Flower Constellations can represent hundreds of spacecraft with a set of 6 integers and 5 real parameters only and existing constellations can be easily reproduced. How to design a Flower Constellation to satisfy specific mission requirements is an important problem for promoting the acceptance of this novel concept by the space community. Therefore one of the main goals of this work is that of proposing design techniques that can be applied to satisfy practical mission requirements. The results obtained by applying Global optimization techniques, such as Genetic Algorithms, to some relevant navigation and Earth observation space-based systems show that the Flower Constellations not only are as effective asWalker Constellations, but can also be applied to non-traditional constellation problem domains, such as regional coverage and reconnaissance.Item Front-page gatekeeping and content trends in 15 large-circulation newspapers(2006-12) Schroeder, Jared C.; Watts, Liz; Chambers, ToddThis study examines the state of gatekeeping and news judgment practices among major daily newspapers in three regions by studying their front-page content offerings. Using a content analysis of the story selections of 15 newspapers (five in each region), the results within each region were compared to those of the others using a set of 12 story topic categories. The newspapers were compared individually and as a group to the findings of a massive Readership Institute study that outlined what readers stated they want from their daily newspapers. The 15 newspapers were chosen because of their circulation, all 15 are among the 30 largest in the country in weekday circulation, and geographic location. The study sought a diverse group of papers in terms of media ownership and most of the nation’s top media markets are represented. Gatekeeping practices are similar, with differences appearing when regional or readership-specific needs arise to change the weights given to different stories. The results also show that in the current newspaper and overall media environment, newspapers that focus their resources on what their readership most values, wants and needs to know, and are easy to navigate will have a chance to compete or at least hold their readership in years to come.