形式化方法是一种建立在严格数学基础上的软件开发方法。在软件开发过程中使用形式化方法，既可以提高目标软件系统的正确性和可靠性，又能提高软件的开发效率。但是，正因为形式方法以严格的数学理论为基础，所以用它来描述的软件需求规格说明比较抽象难懂。而且，一般来说，形式化的规格说明语言都是不可执行的，用户和领域专家对形式化规格说明及其符号方面的知识了解甚少，很难去理解形式化规格说明，也就难以确定规格说明是否与他们的需求相一致。为此，人们提出要对形式化的需求规格说明进行确认和验证。 本文主要研究了软件需求规格说明的一种确认方法——动画模拟技术，并最终研究开发了一个Object-Z规格说明动画模拟系统——OZAnimator，该系统能够模拟执行Object-Z规格说明，帮助人们理解需求规格说明，从而实现对规格说明的一致性确认。 首先，本文为Object-Z规格说明定义了一种通用的XML格式，动画模拟系统将处理满足该格式的Object-Z规格说明。 其次，在结构模拟部分，作者选择SICStusProlog作为动画模拟语言，根据Object-Z规格说明语言的语法语义，制定了一系列由Object-Z规格说明到Prolog文件的转换规则，并使用XSLT描述出来。在动画过程中，输入的Object-Z规格说明将根据这些转换规则自动转换成可执行的Prolog程序。 作者使用Java语言设计了一个良好的动画模拟界面，该界面包含了Obiect-Z规格说明的文档结构、类的属性和变化情况、用户的操作过程以及错误信息的显示，实现了用户与规格说明的交互的需求和进行需求确认的目的。 最后以多个实例对本动画模拟系统进行了测试，证明本系统能够正确有效地模拟执行Object-Z规格说明，并且根据测试结果对这种动画模拟技术进行了相关的讨论。