Sciweavers

Share
ICST
2010
IEEE

When BDDs Fail: Conformance Testing with Symbolic Execution and SMT Solving

9 years 8 months ago
When BDDs Fail: Conformance Testing with Symbolic Execution and SMT Solving
—Model-based testing is a well known technique that allows one to validate the correctness of software with respect to its model. If a lot of data is involved, symbolic techniques usually outperform explicit data enumeration. In this paper, we focus on a new symbolic test case generation technique. Our approach is based on symbolic execution and on satisfiability (modulo theory; SMT) solving. Our work was motivated by the complete failure of a well-known existing symbolic test case generator to produce any test cases for an industrial Session Initiation Protocol (SIP) implementation. Hence, we have replaced the BDD-based analysis of the existing tool with a combination of symbolic execution and SMT solving. Our new tool generates the test cases for SIP in seconds. However, further experiments showed that our approach is not a substitutive but a complementary approach: we present the technique and the results obtained for two protocol specifications, the first supporting our new te...
Elisabeth Jöbstl, Martin Weiglhofer, Bernhard
Added 26 Jan 2011
Updated 26 Jan 2011
Type Journal
Year 2010
Where ICST
Authors Elisabeth Jöbstl, Martin Weiglhofer, Bernhard K. Aichernig, Franz Wotawa
Comments (0)
books