在软件开发过程中,多数用户需求的规格说明采用非形式的自然语言或半形式的图表结构进行描述,由于非形式方法的模糊性和歧义性,产生的规格说明往往不够精确和完整,规格说明的不同使用者对于同一规格说明会有不同的理解,从而造成系统的不完善.形式方法基于严格的数学逻辑,以形式推理和定理证明为工具推导程序,能提供精确的规格说明.形式方法虽然具有精确、无二义性的特点,但由于它需要设计者有较好的数学基础,因此不容易为人们所接受.图形化规格说明和形式方法都可以用于软件开发的需求分析和设计阶段,有很大的互补性.本文就是以UML和Object-Z为例,研究如何在软件需求分析阶段集成图形化规格说明和形式方法,以获得精确的软件需求规格说明.本文从整个系统的角度分析了如何实现从用户需求到图形化规格说明描述,再到形式规格说明:首先结合一个例子,介绍了如何使用UML来描述系统的Use Case视图、Logical视图、Component视图和Deployment视图.接着从这个实例出发,对该模型的Use Case视图和Logical视图进行形式化,系统地研究了UML类图、用例图、顺序图、状态图到Object-Z的转换,在总结前人的基础上,通过形式化各种UML模型中的元模型,提出了自己关于UML到Object-Z的一个比较系统的转换规则.根据本文提出的规则,可以实现一个简单系统的UML规格说明到形式规格说明的转换.为了支持本文提出的理论方法,开发了基于XMI(XML Metadata Interchange)的工具UMLFormalizer,实现了UML模型到Object-Z的自动转换.