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

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

Typ: Seminarthema Betreuer: David Faragó

Links: Paper

In domains where data plays an essential part, specifications with explicit data enumeration often lead to state space explosion. As alternative, symbolic transition systems can be used for specification. Model-based conformance testing can then use new symbolic test case generation techniques based on symbolic execution and on satisfiability (modulo theory; SMT) solving. After some introduction, the paper explains the test case generation algorithm in Section 3, which should be the focus in this seminar. Section 4 gives two case studies (the Conference Protocol and the Session Initiation Protocol used in Voice-over-IP), one of which can optionally be presented.