软件测试是软件生命周期中一个重要环节,直接关系到软件的质量高低,充分的测试是项目成功的重要保障,测试用例的产生是软件测试的关键步骤,因而,软件测试的质量和效率很大程度上决定于测试用例的优劣;完全由人工生成测试用例会耗费较大的人力和财力,并且一般说来项目还有较为严格的时间限制,因此自动生成测试用例就显得十分重要,它可以更加准确且省时的生成测试用例;所以,本文开展自动生成高质量测试用例的研究对于软件测试具有十分重要的理论意义和应用价值。本文首先对国内外在测试用例自动生成领域的研究进行了分析,在此基础上提出了一种自动生成高质量测试用例的方法,研究了如何从用例规格说明来生成Z语言形式规格说明的方法。为了更为准确的描述系统需求本文提出了对用例规约进行精化的方法,精化的用例规约能够在一定程度上减少自然语言描述用例带来的模糊、不精确性。基于精化的用例规约,应用活动图来描述用例,抽象活动图得到有向图,通过遍历有向图的方式获得了所有的用例场景,基于这些用例场景来得到Z语言的形式规格说明。本方法在提高生成形式规格说明的自动化程度方面有所创新。为了便于书写Z规格说明,本文还编写了一个Z规格说明的编辑及类型检查工具。本文研究了基于形式规格说明来生成有效测试用例的方法。具体是由形式规格说明来产生系统的测试用例集合,对测试用例的组织方式进行了研究,提出了用例场景全前置条件最大无环有效覆盖准则及其相应测试用例序列的生成算法,使测试用例对用例场景的覆盖率得到提高,在测试的全面性、有效性方面有所改进和创新。为了检验提出的测试用例覆盖准则的有效性,本文结合一个示例项目与已有的最大无环有效覆盖准则进行了比较,结果显示本文提出的测试序列能够有效的检测前置条件为复杂谓词析取的用例场景实现中的错误。最后,在前面各项工作的基础上,提出了测试用例自动生成工具的框架,并对其各个部分进行了简要阐述。