Model Based Quality Assurance
Our main focus on model-based functional software testing is to address the whole test design problem from choosing input values, generating sequences of operation calls to automated generation of executable test cases. Therefore, we need a dedicated test model (e.g. statecharts) specifying the intended behavior of the System Under Test (SUT) including oracle information. For automated test case generation, structural coverage criteria such as transition coverage are considered to define test goals. A test case generator has to perform reachability queries on the state space of the test model until every test goal is covered. For this computationally expensive task, we investigate different model checking strategies and respective tools. Thereupon, we adapt those concepts to also generate test suites for entire product lines under test by taking the inherent variability of the SUT into account.