1. A method for generating tests for a system under test, comprising: generating a model of the system under test; generating a first test case with respect to the model; adding the first test case to a collection of test cases; checking a coverage metric over the collection of test cases; and if the coverage metric is not satisfied, performing the further steps of: reducing the model; and generating a second test case with respect to the reduced model.