形式规格说明语言基于严密的数学和逻辑，它是精确的，无二义性的语言。形式规格说明语言克服了非形式化语言的二义性，但是它并不能完全避免规格说明中的人为错误。本文研究的是形式规格说明的测试方法。通过研究和比较，测试相比其他形式规格说明的验证方法需要较少的人力、物力，却能达到很好的检测效果。在实际的应用中，测试相比其他的验证方法有更多的工具支持。本文所研究的是基于模型的形式规格说明的测试方法。 常见的基于模型的形式规格说明语言包括Z，Object-Z和VDM，这些基于模型的规格说明语言都是以谓词公式来描述系统功能的。本文提出了从两种角度对基于模型的形式规格说明进行测试：基于谓词错误的测试方法和基于谓词结构的测试方法。 基于谓词错误的测试方法假设形式规格说明的前置条件存在已知类型的谓词错误。本文提出的测试方法是通过选取合适的测试用例使得假设错误的谓词公式和假设正确的谓词公式的结果是异或的，发现前置条件的错误。基于两类谓词错误：表达式否定错误(Expression Negation Fault)和表达式多余错误(Expression Unwanted Fault)，本文分别提出了两种不同的测试准则：ENF测试准则和EUF测试准则。ENF测试准则可以帮助测试人员构造测试用例，发现规格说明前置条件中的ENF错误。相对的，EUF测试准则可以发现前置条件中的EUF错误。基于谓词错误的测试方法可以覆盖谓词公式中所有一类错误的可能性，保证形式规格说明前置条件相对正确性。 基于谓词结构的测试方法是基于覆盖的测试准则。测试人员知道规格说明的前置条件和后置条件，对规格说明进行结构性的覆盖度测试。本文提出了5种不同的覆盖度准则。基于不同覆盖度准则的测试用例可以对形式规格说明的谓词部分有不同的覆盖度。 在测试领域中，测试的自动化是非常重要的。测试自动化是为了节省测试的成本以及简化测试的过程。本文基于谓词错误的测试方法，研究并开发了一套应用于基于模型的形式规格说明的测试工具PredTesting。它可以简化测试的过程，使测试用例生成的过程自动化。PredTesting是基于Java 6.0和Swing图形界面的图形化测试工具。该工具可以把测试用例导出为标准的XML文件格式。本文详细介绍了该工具的基本架构、设计和实现。最后，本文通过一个实例来演示工具的使用。