Integrating the concepts of Formal Methods with Testing can be potential solutions for developing critical systems becoming more and more complex in the automotive field. While Formal Methods provide the benefits by their rigorous nature and their capability of automation, it is still in limited cases to be applied because of 2 major issues: modeling and scalability. Integrating Formal Method concepts with testing techniques are potential solutions in practice. Our approach is to define verification criterion that includes: consistency at the abstraction level of models between generic property (like controllability) and underlying assumptions; and coverage criteria of test cases against the models and underlying assumptions. This approach allows using approximated plant models for the purpose of control system verification. In contrast to model-based testing which is also called specification-based testing in the research field of Software Testing, our approach does not grant the models themselves as the test oracles, but we introduce controllability and underlying assumptions instead in order to derive test oracles. This paper shows a case study of this method applied to a set of the artifact of a product system. The abstract model created in NuSMV is much more compact than the target Simulink model for testing, which has been used for generating embedded software, and the generated test cases are similar to the existing product test cases although they do not properly treat timing and interleaving due to the limitation of the tentative coverage criterion. This result shows potential benefits of the proposing method and reveals the research direction in order to apply the theories and techniques in the model checking field by substituting soundness by testability.