Handling Model Changes: Regression Testing and Test-Suite Update with Model-Checkers

Several model-checker based methods to automated test-case generation have been proposed recently. The performance and applicability largely depends on the complexity of the model in use. For complex models, the costs of creating a full test-suite can be significant. If the model is changed, then in general the test-suite is completely regenerated. However, only a subset of a test-suite might be invalidated by a model change. Creating a full test-suite in such a case would therefore waste time by unnecessarily recreating valid test-cases. This paper investigates methods to reduce the effort of recreating test-suites after a model is changed. This is also related to regression testing, where the number of test-cases necessary after a change should be minimized. This paper presents and evaluates methods to identify obsolete test-cases, and to extend any given test-case generation approach based on model-checkers in order to create test-cases for test-suite update or regression testing.