中文摘要：

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

结论摘要：

UML是当今主流的建模语言，也是工业界的事实标准。然而，由于UML缺乏精确的形式语义，无法实现对系统设计的推理与验证。本研究对UML的形式语义进行研究，给UML赋予统一的、可执行的形式语义框架，主要做了以下工作1）提出了基于情态演算的统一的UML语义框架；2）在定理证明器Coq中实现了UML动态图的指称语义、操作语义，并做了正确性研究，实现了可执行的操作语义；3）研究了设计模式的形式化，对典型设计模式进行了EMF实现；4）提出了可机械验证的软件设计精化思想。总之，我们给UML赋予了统一的、可执行的形式语义框架，从各个方面为UML模型精化与模型测试、验证提供了理论基础。