随着计算机硬件性能迅速提高和价格的持续下降，计算机系统应用范围不断地扩大，软件系统也日益复杂，研究如何提高软件质量和软件开发效率的工作变得日益重要。UML语言已成为软件工程领域事实上的标准建模语言，它提供了丰富的建模机制，并且容易让用户理解，因此在抽取和定义用户需求阶段获得了广泛的应用。但由于UML语言缺乏精确的语义，而使得分析设计人员难以建立精确的需求模型，更难以使用工具对模型自动进行系统的分析和验证。形式方法则是一种基于数学的软件开发方法，形式方法能对系统应该满足的性质进行描述，它具有精确性，一致性和无歧义性等特点，并且能够对规格说明进行分析和验证，因此被认为是提高软件质量的有效方法。然而，在工业界，形式方法大都仅用于安全攸关领域。形式方法被批评为难以使用，费时费力，由于需要分析设计人员具备良好的数学基础和抽象思维能力，因此构建形式规格说明比较困难，并且缺少有效的和完整的工具来支持软件开发人员使用形式方法。在软件的开发过程中怎样才能有效地结合面向对象方法与形式方法则是一个值得研究的课题，本文所做的工作和取得的成果主要体现在以下几个方面：●本文以UML和Object-Z作为建模工具，提出了一种在软件需求阶段结合图形化规格说明和形式方法，以获得精确的软件需求规格说明的方法。本文从整个系统的角度研究了如何实现从用户需求得到图形化规格说明，再到形式规格说明，并对规格说明进行有效确认的方法和技术。●在对图形化规格说明技术与形式方法进行对比分析的基础上，指出了它们的优缺点。通过分析得出了这样的结论：将图形化规格说明与形式方法结合，就能互相弥补双方的缺陷和不足，并能最大限度地发挥出各自的优势。同时本文提出了一种结合图形化方法与形式化方法来构造软件需求规格说明的过程。●在UML与形式方法的结合过程中发挥了补充法和结合法的综合优势，首先根据补充法的原则使用OCL对模型信息进行较为精确的描述，再使用结合法，即通过将带OCL约束信息的UML模型转换为Object-Z规格说明使UML模型形式化。使用Object-Z就可以方便地表达面向对象的概念。在总结现有研究成果的基础上，通过分析现有研究成果中的不足之处，系统地提出了一整套从UML类图，状态图以及用例图到Object-Z规格说明的转换规则，并用一个电梯系统的实例加以说明。●在结合UML与Object-Z的研究过程中，发现OCL语言与Object-Z语言具有很强的互补性，给出了从OCL表达式系统地转换到Object-Z规格说明的方法。本方法结合了UML／OCL模型直观性与Object-Z语言的严密性优点，可产生更为完全的Object-Z规格说明。为了支持本文提出的方法，又开发了基于XMI的工具UMLFormalizer，初步实现了从UML模型到Object-Z的自动转换。●目前常见Object-Z存储交换格式有基于Latex和基于XML格式两种，本文在对这两种常见存储交换格式进行分析比较的基础上，认为采用XML格式的Object-Z规格说明文件更有利于形式开发工具的集成，并且对现有的Object-Z规格说明的XML描述进行改进，从而完善了其操作部分，使用XML模式定义了一个Object-Z的XML标记格式，给出了该XML结构的具体定义。●在Object-Z规格说明动画技术研究方面，我们提出了一种形式化规格说明的动画模拟技术确认方法，并设计开发出Object-Z规格说明的一个动画模拟系统——OZAnimator，以便帮助用户对形式规格说明进行确认。