软件测试是保证软件产品可靠性和正确性的有效方法，其中设计和生成有效的测试用例是决定测试质量的重要因素之一，而测试用例自动生成可以节省测试时间，降低开发成本。模型检验是确保软件设计正确性的形式化验证技术。给出系统有限状态模型和性质的逻辑表达，模型检验能自动检验该性质在这个模型上是否成立，特别是当某条时序逻辑公式不成立时，能够自动地抛出一条执行路径来表明系统并不满足这条性质，称这条路径为反例。模型检验工具自动生成反例的功能，可以用于实现测试用例生成自动化。近年来，人们对使用模型检验自动生成测试用例进行了研究，使之在变异测试、结构化测试、数据流测试、类测试方面得到应用。 本文在已有工作基础上，总结归纳了模型检验技术用于测试用例生成的若干种方法框架，完善了基于模型检验生成数据流测试用例的方法，提出了一种基于模型检验的类测试用例生成方法。论文主要工作包括： (1)使用时序逻辑描述结构化覆盖标准，并证明了时序逻辑描述与相应覆盖标准的等价性； (2)提出一种基于模型检验技术的过程内数据流异常检测方法，该方法不仅可以检测出程序中的数据流异常，还能给出引起每条异常的执行路径； (3)提出一种使用模型检验生成类测试用例的方法，该方法是利用符号执行从类源代码抽取对象的状态和行为，以一个四元组抽象描述类，并转化成等价的Kripke结构。使用计算树逻辑描述相应的测试覆盖标准，模型检验生成反例的功能可使类测试用例生成自动化，实验表明生成的测试用例具有较高的覆盖率。