Abstract: It is a breakthrough to use model checking technique to automatically generate test cases. For infinite states systems with input/output domains defined on unbounded and abstract types, the function of general model checking technique is very restricted in generating test cases. This paper presents the idea of auto-generation of test cases based on symbolic execution and LTL temporal formula rewriting method. The method proceeds with building the symbolic representation of program execution model, such that it can avoid explicitly building the model of infinite states systems with the enumeration of value of input and output or state explosion problem. Then temporal formula (test purposes) rewriting is applied to the symbolic execution model of program to generate complex constraint requirements according to the counterexample patterns related to test purposes and the suitable SMT(satisfiability modulo theory) solver is called for generating test cases. At the level of syntax, IOSTS and LTL formulae are used to specify interactive behaviors of systems under testing and test purposes, respectively. Therefore, the approach has the advantages of modeling the abstract behaviors and data dependence as well as defining all kinds of test requirements concisely and naturally in a rigorous means. Further, the paper designs the algorithm for LTL formula rewriting engine, which computes the necessary condition satisfied by test cases related to the targeted test purposes. At last, a case study is conducted for showing the usefulness of the method.