UML是当今主流的建模语言，也是工业界的事实标准。然而，由于UML缺乏精确的形式语义，无法实现对系统设计的推理与验证。本项目将对UML的形式语义进行研究，给UML赋予统一的、可执行的形式语义框架。首先给UML赋予统一的、抽象的指称语义。指称语义将UML中各种非形式语义的元素形式化为抽象的数学元素（函数、集合等）。将提出一个统一的指称语义模型作为UML形式语义的框架。其次，基于该指称语义框架，给UML赋予基于元模型的操作语义。操作语义是指称语义的实现，能给UML带来可执行性，实现对UML模型的测试与验证等实际应用。将采用元模型织入的方法，在UML元模型中织入其操作语义。最后，证明指称语义与操作语义的等价。将利用定理证明器Coq，通过对两种语义进行描述，并采用结构归纳证明两种语义之间的等价性。总之，将给UML赋予统一的、可执行的形式语义框架，为UML模型精化与模型测试、验证提供理论基础。