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...

• Type: Journal
• Year: 2010
• Where: ICST
• Authors: Elisabeth Jöbstl, Martin Weiglhofer, Bernhard K. Aichernig, Franz Wotawa
• Keywords: ICST 2010, Software Engineering, Symbolic Execution, Symbolic Input-output Conformance, Symbolic Test Case