Powered by
Conference Publishing Consulting

6th International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2014), May 31, 2014, Hyderabad, India

CSTVA 2014 – Proceedings

Contents - Abstracts - Authors

6th International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2014)


Title Page

Message from the Chairs
Welcome to CSTVA 2014, the 6th workshop on Constraints in Software Testing, Verification and Analysis, held on 31st May 2014 at Hyderabad, India, as a workshop of the ICSE 2014 conference. Recent years have seen an increasing interest in the application of constraint-solving techniques to testing, verification and analysis of software systems. The reason for this interest is the dramatic improvement in efficiency and expressive power of Boolean SAT, SMT and CP solvers, thus making it considerably easier to build and maintain these applications. As the solvers become more efficient and expressive, newer applications are being developed in diverse areas of software engineering (SE). Moreover, rather than just using solvers as black boxes, a recent trend in solver-based SE applications is a deeper integration of solver and application. This can result in more powerful SE techniques but it necessitates close interaction between solver developers and users. The aim of this workshop is to highlight the use of solvers in novel applications, new solver features, and encourage the use of solvers in fresh solutions to long-standing SE problems. Furthermore, the workshop should act as a venue for cross-community interaction between researchers in constraint solving and in software engineering.

Fast Abstracts

Directed Test Suite Augmentation via Exploiting Program Dependency
Haijun Wang, Xiaohong Guan, Qinghua Zheng, Ting Liu, Chao Shen, and Zijiang Yang
(Xi'an Jiaotong University, China; Xi’an University of Technology, China; Western Michigan University, USA)
Regression testing is a practice to discover faults introduced in the program modification. However, the existing test suite is usually designed at an early stage of software development and is therefore insensitive to subsequent program changes. Although symbolic execution such as JPF-SE is able to produce test cases for the modified program by exhaustively exploring program paths, it is not tailored for testing program changes and is not scalable. In this paper, we propose an efficient approach called Directed Test Suite Augmentation (DTSA) to automatically generate test cases that can reach the changed statements, produce different program states after executing the changed statements, and propagate the different states to the output of the program. The key insight of DTSA is to reorder the generated test cases tailored for testing program changes compared with JPF-SE. We implemented a prototype of our approach and the experiment results show that DTSA requires about 60.1% and 45.6% fewer Dynamic Symbolic Execution (DSE) runs to generate the desired test case than JPF-SE and another test suite augmentation tool eXpress, respectively.

Publisher's Version Article Search
Generating Test Cases inside Suspicious Intervals for Floating-Point Number Programs
Hélène Collavizza, Claude Michel, Olivier Ponsini, and Michel Rueher
(University of Nice Sophia Antipolis, France; CNRS, France)
Programs with floating-point computations are often derived from mathematical models or designed with the semantics of the real numbers in mind. However, for a given input, the computed path with floating-point numbers may differ from the path corresponding to the same computation with real numbers. State-of-the-art tools compute a over-approximation of the error introduced by floating-point operations with respect to the same sequence of operations in an idealized semantics of real numbers. Thus, totally inappropriate behaviors of a program may be dreaded but the developer does not know whether these behaviors will actually occur, or not. We introduce here a new constraint-based approach that searches for input values hitting the part of the over-approximation where errors due to floating-point arithmetic would lead to inappropriate behaviors. Preliminary results of experiments on small programs with classical floating-point errors are very encouraging.

Publisher's Version Article Search
Towards Testing of Full-Scale SQL Applications using Relational Symbolic Execution
Michaël Marcozzi, Wim Vanhoof, and Jean-Luc Hainaut
(University of Namur, Belgium)
Constraint-based testing is an automatic test case generation approach where the tested application is transformed into constraints whose solutions are adequate test data. In previous work, we have shown that this technique is particularly well-suited for testing SQL applications, as the semantics of SQL can be naturally transformed into standard SMT constraints, using so-called relational symbolic execution. In particular, we have demonstrated such testing to be possible in practice with current solver techniques for small-scale applications. In this work, we identify the main challenges and provide research directions towards constraint-based testing of full-scale SQL applications. We investigate the additional research work needed to integrate relational and dynamic symbolic execution, handle properly dynamic SQL, generate tractable SMT constraints for most SQL applications, detect SQL runtime errors and deal with non-deterministic SQL.

Publisher's Version Article Search

Research Papers

Model-Based Optimization of Automotive E/E-Architectures
Stefan Kugele and Gheorghe Pucea
(TU München, Germany)
In this paper we present a generic framework to enable constraint-based automotive E/E-architecture optimization using a domain-specific language. The quality of today's automotive E/E-architectures is highly influenced by the mapping of software to executing hardware components: the so-called deployment problem. First, we introduce a holistic architectural model facilitating a seamless model-based development from requirements management to deployment, which is the focus of this work. Second, we introduce our domain-specific constraint and optimization language AAOL (Automotive Architecture Optimization Language) capable to express a wide range of deployment-relevant problems. Third, we present a generic, i.e., solver-independent framework currently supporting multi-objective evolutionary algorithms (MOEA). We investigate the feasibility of the approach by dint of a case study taken from the literature.

Publisher's Version Article Search
Automatic Repair of Buggy If Conditions and Missing Preconditions with SMT
Favio DeMarco, Jifeng Xuan, Daniel Le Berre, and Martin Monperrus
(Universidad de Buenos Aires, Argentina; INRIA, France; University of Artois, France; CNRS, France; University of Lille, France)
We present Nopol, an approach for automatically repairing buggy if conditions and missing preconditions. As input, it takes a program and a test suite which contains passing test cases modeling the expected behavior of the program and at least one failing test case embodying the bug to be repaired. It consists of collecting data from multiple instrumented test suite executions, transforming this data into a Satisfiability Modulo Theory (SMT) problem, and translating the SMT result -- if there exists one -- into a source code patch. Nopol repairs object oriented code and allows the patches to contain nullness checks as well as specific method calls.

Publisher's Version Article Search
Suitability Analysis of CSP- and SMT-Solvers for Test Case Generation
Hermann Felbinger and Christian Schwarzl
(Virtual Vehicle Research Center, Austria)
Model-based testing allows automatic test case generation from models like Symbolic Input Output Transition Systems (SIOTS) describing the behavior of the System under Test (SUT). In order to create feasible test inputs a Constraint Satisfaction Problem (CSP)-solver or a Satisfiability Modulo Theory (SMT)-solver can be used. The test input creation complexity depends amongst others on the variable domains, the variable number and the test length. Since the capabilities of a test generation from a given SIOTS strongly depends on the used CSP- or SMT-solver, the most suitable one has to be selected. In this paper we benchmarked commonly used CSP- and SMT-solvers like Minion, Choco, Z3 or CVC4, regarding their time needed to solve constraints typical in model-based testing. The experimental results show that the compared solvers can differ vastly regarding the number of correctly solved and the time needed for a set of constraints. Since the solver performance depends on the characteristics of the constraint to be solved, no winner can be named. However, the provided results allow the selection of the most suitable solver for dedicated problem sets.

Publisher's Version Article Search

proc time: 0.48