统一建模语言(UML, Unified Modeling Language)是一种非专利的可视化建模和规约语言。UML提供了开放的方法,用于系统说明、文档化、可视化构建面向对象的软件密集系统。然而UML并没有被赋予严格的形式化语义,而且对于动态模型仅仅只能描述而无法执行,这使得模型的验证成为一个难题。造成软件系统的许多缺陷在软件设计开发初期很难发现,导致开发成本的增加。相对而言,Petri网拥有丰富的理论基础,严格的形式化语义,而且是一种可执行的模型。本文着眼于两种模型的优势,将UML模型中的状态图转换为Petri网模型,进而通过对Petri网模型的分析验证达到确保原模型正确性和合理性的目的。本文首先针对UML和Petri网两种模型映射的国内外研究现状进行了分析和综述,基于相关的Petri网基础理论,在研究UML状态图向Petri网映射的方法中,以图模型为基础,提出了具体的映射规则,然后对映射规则的正确性进行了形式化证明,以确保二者语义上的等价性。在完成两种模型的映射基础上,设计开发了二者的自动转换工具,并通过一个实例讨论和分析了转换工具的工作流程合理性。本文以设计一个小型网络购物系统为实例,首先基于VP-UML设计系统的用例图、类图以及订单对象的状态图；然后针对订单对象状态图,采用本文所提出的方法,使用自动转换工具将其转为Petri网模型；最后根据Petri网理论对该模型进行相关的性质分析和行为验证。通过实例验证了映射方法的可行性和正确性。本文的主要工作和创新之处在于将UML模型以可执行模型的形式予以处理和展现,采取将UML模型映射为Petri网的方式,并从两个方面,即理论证明和实例验证,确保了映射规则和转换的正确性。网络购物系统的实例也证明该方法在软件设计与开发的实际工作中的适用性,显现出对于提高软件系统的正确性和可靠性的作用。