作为一种定义良好、功能强大的图形化建模语言，UML因为缺乏精确的语义描述，因此对系统的建模无法进行形式化的分析和验证。目前，已经有很多UML形式化的研究成果，但都存在一定的局限性。本文在分析UML建模图特点的基础上，选择Petri网作为UML建模图转换的形式化规范，一是因为Petri网也采用图形表示，可以从UML图形直接转换而来作为分析验证的工具，这样避免了形式化方法对数学基础要求较高，直接使用起来建模困难的局限性；二是因为Petri网有一整套严格的理论分析方法和工具，弥补了UML缺少模型分析、验证手段的不足。 本文中，我们主要针对UML顺序图和类图，分别给出了二者的Petri网建模方法。对于UML顺序图，由于其表达能力有限，我们先对其进行了相应的扩展，使得消息传递机制中的几种特殊关系，如并发、选择、同步等能够通过扩展顺序图表达清楚，进而给出了扩展顺序图转换为Petri网时的九种转换规则；而对于类图，由于类图中定义了类的属性和操作以及类之间的关联关系，是各种动态行为图的基础，通过分析类图主要元素的特点，我们选择有色Petri网作为其形式化的规范，分析了UML类图和有色Petri网元素之间的对应关系以及转换前类图应满足的特定形式，最后给出了类图到有色Petri网具体的转换方法。从而通过转换，分别得到两种模型图基于Petri网的可执行模型，实现了UML模型图的形式化。