软件测试作为保证软件质量，提高软件可靠性的重要手段，在软件开发中起着不可替代的作用，其关键与核心是测试用例的生成。目前测试用例的生成主要靠手工完成，测试过程往往带有很大的盲目性，致使测试效率低下，软件成本居高不下，软件质量也很难得到保证。为此，迫切需要改进软件测试的方法，开发一些测试用例的自动生成工具，提高软件测试效率，降低软件测试成本，保证软件质量，提高软件测试的自动化程度。 文中探讨了基于软件形式化规格说明自动生成测试用例的方法和技术，提出了一种新的方法：以Z语言描述软件的规格说明，借助于分类树生成工具CTE XL得到高层的测试用例，再利用析取范式方法进一步细化测试用例，得到以析取范式形式存在的谓词序列。最后采用1×1域测试策略得到具体的测试用例。 改进了兰毓华提出的测试用例生成流程，结合分类树和析取范式方法得到细化的高层测试用例。由形式化规格说明得到的分类树是完全形式化的，因为每个被选择类都是形式化的谓词，因此被选择类的形式化描述可以由它们的谓词以一种直接的方式自动得到。DNF方法的一个显著优点是它是完全基于语法的，所以可以由形式化方法规格说明自动得到。得到的测试用例覆盖了测试对象的所有需测试方面，包括输入信息和输出信息。 应用属于白盒测试范围的针对域错误的测试数据生成算法寻找具体的测试值，解决了复杂谓词和非线性谓词产生测试用例难的问题。