Narrow Results

We show how to solve boolean combinations of inequations s>t in the Herbrand Universe, assuming that ≥ is interpreted as a lexicographic path ordering extending a total precedence. In other words, we prove that the existential fragment of the theory of a lexicographic path ordering which extends a total precedence is decidable.

Many testing methods are based on program paths. A well-known problem with them is that some paths are infeasible. To decide the feasibility of paths, we may solve a set of constraints. In this paper, we describe constraint-based tools that can be used for this purpose. They accept constraints expressed in a natural form, which may involve variables of different types such as integers, Booleans, reals and fixed-size arrays. The constraint solver is an extension of a Boolean satisfiability checker and it makes use of a linear programming package. The solving algorithm is described, and examples are given to illustrate the use of the tools. For many paths in the testing literature, their feasibility can be decided in a reasonable amount of time.

With the increasing complexity of software, new access control methods have emerged to deal with attribute-based authorization. As a standard language for specifying attribute-based access control policies, XACML offers a number of rule and policy combining algorithms to meet different needs of policy composition. Due to their variety and complexity, however, it is not uncommon to apply combining algorithms incorrectly, which can lead to unauthorized access or denial of service. To solve this problem, this paper presents a fault-based testing approach for revealing incorrect combining algorithms in XACML 3.0 policies. The theoretical foundation of this approach relies on the formalization of semantic differences between rule combining algorithms and between policy combining algorithms. It allows the use of a constraint solver for generating queries to which a given policy produces different responses than its combining algorithm-based mutants. Such queries can determine whether or not the given combining algorithm is used correctly. Our empirical studies using various XACML policies have demonstrated that our approach is effective.

Test data generation is a process of creating program inputs that satisfy specific testing criteria. Many works have been focused on test generation with respect to numeric and string data. Dynamic data structures, such as trees and linked lists, have been widely used in modern programming, but on which there are few studies presented. In general, generating a dynamic data structure is associated with a proper shape and valid values generation. It would be difficult to generate such dynamic data structures, as both shapes and values are necessary to be valid simultaneously. This paper focuses on binary tree structures and proposes a novel test generation approach that combines search based testing with constraint solving techniques. The approach creates the shapes of binary tree structures by using GA, and generates the values in their data fields by using constraint solving techniques. The experimental results show that the presented approach is promising and effective. Moreover, the studies investigate factors affecting the performance of the approach, and arrive at a conclusion that the test generation cost is cubic growing as the number of pointer constraints increases.

Multi-objective evolutionary algorithm (MOEA) has been widely applied to software product lines (SPLs) for addressing the configuration optimization problems. For example, the state-of-the-art SMTIBEA algorithm extends the constraint expressiveness and supports richer constraints to better address these problems. However, it just works better than the competitor for four out of five SPLs in five objectives and the convergence speed is not significantly increased for largest Linux SPL from 5 to 30min. To further improve the optimization efficiency, we propose a parallel framework SMTPORT, which combines four corresponding SMTIBEA variants and performs these variants by utilizing parallelization techniques within the limited time budget. For case studies in LVAT repository, we conduct a series of experiments on seven real-world and highly-constrained SPLs. Empirical results demonstrate that our approach significantly outperforms the state-of-the-art for all the seven SPLs in terms of a quality Hypervolume metric and a diversity Pareto Front Size indicator.

An effective method for addressing the configuration optimization problem (COP) in Software Product Lines (SPLs) is to deploy a multi-objective evolutionary algorithm, for example, the state-of-the-art SATIBEA. In this paper, an improved hybrid algorithm, called SATIBEA-LSSF, is proposed to further improve the algorithm performance of SATIBEA, which is composed of a multi-children generating strategy, an enhanced mutation strategy with local searching and an elite inheritance mechanism. Empirical results on the same case studies demonstrate that our algorithm significantly outperforms the state-of-the-art for four out of five SPLs on a quality Hypervolume indicator and the convergence speed. To verify the effectiveness and robustness of our algorithm, the parameter sensitivity analysis is discussed and three observations are reported in detail.

Generating faulty data is a key issue in fault injection. The faulty data include not only the ones of extreme values or bad formats, but also the ones which are logically unreasonable. Constraint-based fault injection which negates interface constraints to solve faulty data is effective for logically unreasonable data generation. However, the existing constraint-based approaches just solve brand new data for testing. Such brand new data may easily violate some hidden environment constraints on the test inputs and hence be nonrealistic. Besides, there can be different strategies to negate a constraint in order to derive the constraint-unsatisfied faulty data. What are the possible negation strategies and which strategies are better for high coverage fault injection are still unclear. To these ends, this paper presents a new constraint-based fault injection approach. The approach introduces 10 different strategies for constraint negation and relaxes constraint variables to generate faulty data instead of solving brand new data for fault injection. It can produce faulty data which are closer to the original non-faulty ones and hence likely to be more realistic. We experimentally investigated the effectiveness and cost of the introduced constraint negation strategies. The results provide insights for the application of these strategies in fault injection.

A general approach to implement propagation and simplification of constraints consists of applying rules over these constraints. However, a difficulty that arises frequently when writing a constraint solver is to determine the constraint propagation algorithm. In previous work, different methods for automatic generation of rule-based solvers for constraints defined over finite domains have been proposed^1,2,3,4. In this paper, we present a method for generating rule-based solvers for constraint predicates defined by means of a constraint logic program, even when the constraint domain is infinite.