|
Abstract:
|
As software systems grow in complexity , the need for efficient automated techniques for design , testing and verification becomes more and more critical . Specification -based testing provides an effective approach for checking the correctness of software in general . Constraint -based analysis using specifications enables checking various rich properties by automating generation of test inputs . However , as specifications get more complex , existing analyses face a scalability problem due to state explosion . This dissertation introduces a novel approach to analyze declarative specifications incrementally ; presents a constraint prioritization and partitioning methodology to enable efficient incremental analyses ; defines a suite of optimizations to improve the analyses further ; introduces a novel approach for testing software product lines ; and provides an experimental evaluation that shows the feasibility and scalability of the approach . The key insight behind the incremental technique is declarative slicing , which is a new class of optimizations . The optimizations are inspired by traditional program slicing for imperative languages but are applicable to analyzable declarative languages , in general , and Alloy , in particular . We introduce a novel algorithm for slicing declarative models . Given an Alloy model , our fully automatic tool , Kato , partitions the model into a base slice and a derived slice using constraint prioritization . As opposed to the conventional use of the Alloy Analyzer , where models are analyzed as a whole , we perform analysis incrementally , i .e . , using several steps . A satisfying solution to the base slice is systematically extended to generate a solution for the entire model , while unsatisfiability of the base implies unsatisfiability of the entire model . We show how our incremental technique enables different analysis tools and solvers to be used in synergy to further optimize our approach . Compared to the conventional use of the Alloy Analyzer , this means even more overall performance enhancements for solving declarative models . Incremental analyses have a natural application in the software product line domain . A product line is a family of programs built from features that are increments in program functionality . Given properties of features as firstorder logic formulas , we automatically generate test inputs for each product in a product line . We show how to map a formula that specifies a feature into a transformation that defines incremental refinement of test suites . Our experiments using different data structure product lines show that our approach can provide an order of magnitude speed -up over conventional techniques . |