Test Case Generation from Clafer Models; Generation of Abstract Models from Test Cases

Problem: We noticed that Clafer models may be used to create test cases for given specification. A single Clafer model represents many different configurations (e.g. test cases). Automatic generation of various test cases would allow, for example, business analysts to verify whether those cases are correct or not. Furthermore, a number of test cases for a model might be abstracted to a single Clafer model. A single model gives a high-level picture of the test-case suite.

The goal of the project is to provide:

• Implement automatic generation of test cases that are significantly different. The test cases may include only a part of Clafer model.
• Implement abstraction induction, i.e., automatic abstraction of Clafer models from test cases. A fully automatic abstract induction may be impossible for many models. Therefore the user should be able to guide the process.
• Help with under/over-constraining.