软件需求分析是软件开发过程中的首要工作,其分析结果是否准确可靠,将直接影响软件产品的质量,甚至决定了项目的成败。而其中的需求分析方法成为能否有效提高需求分析质量乃至最终软件产品质量的关键因素。UML是软件开发过程中广泛使用的建模语言。但由于它是一种半形式化的建模语言,缺乏精确的语义,用它建立的软件需求模型一方面在用户需求的语义描述上会存在歧异问题,另一方面也难以直接精化和验证,无法进一步提高软件的正确性和可靠性。因此,UML有必要在形式化方面进行拓展。本文探讨了一种利用Object-Z和Perfect对基于UML的需求建模进行形式化分析的方法。其核心思想是:首先,利用Object-Z对UML元模型层上的UML类图的语法和静态语义进行形式化描述,并在UML和Object-Z两者元模型之间寻求一种映射和转换机制;接着在Object-Z和Perfect的元模型之间建立一种映射,并定义它们之间的转换规则,从而实现利用Perfect对Object-Z描述进行精化。这样,既可以保留利用UML进行系统分析设计时强大的系统建模能力和简洁明了的面向对象模型表示法,又能够对UML建立的需求模型进行形式化描述、精化和验证。通过对UML建立的企业人事系统和自动检票系统的需求模型的形式化描述与精化,进一步说明了该方法在实际应用中的可行性。本文的研究结果表明:将UML、Object-Z和Perfect相结合而得到的一种新的软件需求描述方法,能够更好地满足规模和复杂性均不断增大的软件系统的分析、设计和开发等需要,在一定程度上有助于提高软件的正确性和可靠性。