为UML提供坚实的形式化基础是近年来UML研究的热点之一。UML是一种可视化的通用的面向对象建模语言。但是目前UML的语义仍是半形式化的，它是建立在元模型和对象约束语言(OCL，ObjectConstraintLanguage)基础之上的。元模型本身在UML中表达，是UML的一个子集，它定义了UML中的各种图，这是一个循环解释的过程。OCL使用文本方式来描述图上的约束，以提供语义信息。这种半形式化的语义降低了UML模型的精确性，给模型的自动分析和验证带来了困难，一个解决方法就是使用某种形式化方法来精确的描述UML模型图的部分语义信息。 本文主要研究如何使用形式规约语言COOZ来描述部分UML模型。COOZ(CompleteObject-OrientedZ)是定义良好的、面向对象的形式规约语言，它具有足够的表达能力。为了使形式化工作能够尽可能系统化，先用COOZ类模式定义元模型层的模型结构，在此基础上将UML模型转换为COOZ规约。该方法不但为UML提供了较为坚实的形式化基础，给出了UML部分模型的精确描述，也使模型的推理和验证成为可能。 围绕用COOZ形式描述UML部分模型，本文做了如下工作： 1)探讨了UML形式化的意义和方法。先介绍了UML的四层元模型结构以及语言的组织，并论述了UML语义定义上的不精确性。接着研究了仅在模型层进行转换的不足，使用先在元模型一层提供UML模型结构的精确的语法语义描述、再对模型进行形式化描述的方法。 2)对UML的类图进行了形式化。用COOZ的模式表示出模型结构的语法结构，同时将语法约束和静态语义约束用COOZ类的不变式表示，并结合实际的例子说明UML类图到COOZ规约的转换。 3)对UML的状态图进行了形式化。先采用类图形式化的技术将模型结构的抽象语法和静态语义约束表示出来，接着再往相应的COOZ模式中加入表示指称语义的变量和表示操作语义的操作模式，然后用时序逻辑公式给出了操作的次序，最后结合一个例子说明模型层的形式化。