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

Frontmatter

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.

@InProceedings{CSTVA14p1, author = {Haijun Wang and Xiaohong Guan and Qinghua Zheng and Ting Liu and Chao Shen and Zijiang Yang}, title = {Directed Test Suite Augmentation via Exploiting Program Dependency}, booktitle = {Proc.\ CSTVA}, publisher = {ACM}, pages = {1--6}, doi = {}, year = {2014}, }

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.

@InProceedings{CSTVA14p7, author = {Hélène Collavizza and Claude Michel and Olivier Ponsini and Michel Rueher}, title = {Generating Test Cases inside Suspicious Intervals for Floating-Point Number Programs}, booktitle = {Proc.\ CSTVA}, publisher = {ACM}, pages = {7--11}, doi = {}, year = {2014}, }

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.

@InProceedings{CSTVA14p12, author = {Michaël Marcozzi and Wim Vanhoof and Jean-Luc Hainaut}, title = {Towards Testing of Full-Scale SQL Applications using Relational Symbolic Execution}, booktitle = {Proc.\ CSTVA}, publisher = {ACM}, pages = {12--17}, doi = {}, year = {2014}, }

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.

@InProceedings{CSTVA14p18, author = {Stefan Kugele and Gheorghe Pucea}, title = {Model-Based Optimization of Automotive E/E-Architectures}, booktitle = {Proc.\ CSTVA}, publisher = {ACM}, pages = {18--29}, doi = {}, year = {2014}, }

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.

@InProceedings{CSTVA14p30, author = {Favio DeMarco and Jifeng Xuan and Daniel Le Berre and Martin Monperrus}, title = {Automatic Repair of Buggy If Conditions and Missing Preconditions with SMT}, booktitle = {Proc.\ CSTVA}, publisher = {ACM}, pages = {30--39}, doi = {}, year = {2014}, }

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.

@InProceedings{CSTVA14p40, author = {Hermann Felbinger and Christian Schwarzl}, title = {Suitability Analysis of CSP- and SMT-Solvers for Test Case Generation}, booktitle = {Proc.\ CSTVA}, publisher = {ACM}, pages = {40--49}, doi = {}, year = {2014}, }

proc time: 0.71