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 technique, the second being witness for the classic BDD-technique.

Generating test input data is a complex task and nowadays mostly tackled with random approaches. Random testing of methods, which take non primitive data types as parameters, e.g. objects encapsulating database interactions, is a vain endeavor. Especially, if the precondition of the method under test (MUT) requires a particular object state of the method's parameters, random approaches rarely succeed. In this paper we present a technique to automatically synthesize implementations for the parameters of a MUT from a given Design by Contract specification. These implementations behave as described by the Design by Contract specification, but do not interact with their environment (e.g. database, network and file system). Furthermore, we can set the initial state of the synthesized implementations to the state required by the MUT's precondition. Besides a formal discussion of our approach we present results obtained by applying our technique to two case studies: a stack-based calculator and a real-world data collection tool from the telecommunication industry. The presented approach outperforms random data generation on both case studies in terms of amount of methods tested (function coverage) and line coverage.

Model-based test case generation allows one to derive almost arbitrary numbers of test cases from models. If resulting test suites are executed against real implementations, there are often huge numbers of failed test cases. Thus, the analysis of the test execution, i.e. the identification of failures for error reporting, becomes a tedious and time consuming task. In this paper we investigate a technique for grouping test runs that most likely reveal the same failure. This reduces the post analysis time and enables the generation of small regression test suites. The test case grouping is implemented by means of spectrum-based fault localization at the level of the specification. We calculate the grouping by relating the spectra of the test cases. Besides a brief discussion of our approach we present results of applying our approach to the Session Initiation Protocol.

Various research prototypes and a well-founded theory of model based testing (MBT) suggests the application of MBT to real-world problems. In this article we report on applying the well-known TGV tool for protocol conformance testing of a Session Initiation Protocol (SIP) server. Particularly, we discuss the performed abstractions along with corresponding rationales. Furthermore, we show how to use structural and fault-based techniques for test purpose design. We present first empirical results obtained from applying our test cases to a commercial implementation and to a popular open source implementation of a SIP Registrar. Notably, in both implementations our input output labeled transition system model proved successful in revealing severe violations of the protocol.