Test case generation from formal models through abstraction refinement and model checking
Manoranjan Satpathy, S. Ramesh · 2007
In this paper, we adapt the abstraction refinement techniques of Clarke et al. [7] and Gulavani et al. [15] for systematic generation of model based test cases. Formal models are in general infinite state machines. We approximate such a formal model by a more abstract finite state machine. From the finite model, we obtain probable test cases through model checking, and then a guided symbolic execution is performed over the given formal model to check if this is a real test case. In case of failure, the finite abstract model is refined and the cycle is repeated. The two main results of this paper are: (a) better specification coverage is achieved, and (b) we obtain a more accurate coverage estimate. We explain our method by considering models in the specification language B.