随着信息技术的发展，软件规模不断扩大，而且越来越复杂，如何保证和提高软件质量成为软件界最为关心的问题之一。软件测试作为保证软件质量的关键技术，能够有效地发现软件中的故障。对于某些安全关键的软件，其测试费用是所有其它软件工程阶段费用总和的三到五倍。因而，提高软件测试的有效性和测试效率、降低软件开发成本己成为软件工程师迫切需要解决的任务之一。 测试用例的好坏直接影响软件测试的效果。根据测试用例产生的依据可以将软件测试分为白盒测试和黑盒测试，从规格说明产生测试用例的方法称为黑盒测试。形式的软件规格说明具有精确的符号表示和清晰的语义，能够进行推理和证明，同时也便于工具的处理。因此，用形式的规格说明作为测试用例的来源将会使得测试用例的自动构造成为可能。 目前基于Object-Z的形式规格说明构造测试用例的研究主要集中在理论研究阶段，测试用例的自动生成几乎没有相应的工具支持，这主要是因为Obiect-Z是基于数学和逻辑的语言，比较难以提取其中表达式的语义，这就难以自动产生测试用例。本文研究从Object-Z规格说明产生测试用例的自动化过程，这一过程主要包含三个阶段：Object-Z语言的自动解析、语义自动抽取和测试用例自动产生。 本文针对操作模式中使用的调用模式提出了产生测试用例的方法和若干测试准则，该方法能够验证代码中的函数是否正确地调用了其他类的函数。 本文对Object-Z语言的部分文法进行了改进，以减少自动解析时的冲突，提出并完善了用于从Object-Z图形与数学符号结合的语言转换成易于计算机处理的纯文本LaTeX语言的方法，并构造了相应的文法来解析用Object-Z编写的规格说明，生成语法树，根据语法树可以提取出相关语义。为了人们方便地编写和阅读规格说明，Object-Z语言使用了大量的模式复合和简写形式，这给计算机提取完整语义自动产生测试用例造成了困难，因此本文还给出了还原完整语义的方法。 本文实现了提取规格说明中操作模式前置条件的方法，并分离出文字集及它们之间的逻辑关系。本文实现了产生符合组合测试准则和一系列调用测试准则的测试用例的方法。通过本文所提供的软件开发平台，可以很容易得到规格说明中存在的各种语义，方便地实现基于测试准则自动产生测试用例的工具。