随着软件在人们生活中起着越来越重要的作用,如何提高软件的质量,保证软件的可靠性和安全性成为一个重要的问题。在软件设计领域,UML成为广泛运用的软件建模工具,但是UML作为一种半形式化语言,缺乏精确的描述和形式化定义,很难验证模型的正确性。Petri网既是一种图形化建模工具,又是具有严格的语法语义定义的形式化方法,不但能有效地对系统进行描述和建模,对系统的并发性、异步性和不确定性也有很强的动态分析能力。通过将UML模型转化为Petri网模型,再利用Petri网的分析验证技术,可以实现对软件模型的正确性的验证,在设计阶段即发现系统的缺陷,从而减少软件开发后期才发现设计的错误而带来的损失,提高系统的正确性和安全性。本文提出一种系统层次上的对UML状态图进行验证的方法,将UML状态图转换为系统层上的Petri网,然后使用模型检测的方法验证UML状态图转换得到的Petri网模型。并且通过验证状态图转换得到的Petri网模型是否满足协作图描述的用例而验证协作图,从而验证系统的动态行为。本文通过将UML模型的XMI格式进行解析,使用DOM API实现了UML模型向Petri网标识语言PNML自动转换。PNML可以被Petri网建模工具CPNTools识别,从而对转换得到的Petri网模型进行分析和模型验证。CPN Tools提供了一个可视化的界面,可以对Petri网模型进行编辑和仿真,同时也可以验证模型是否满足ASK-CTL公式描述的性质。最后,本文通过实例测试了在Borland Together,CPN Tools等环境下的转换过程和验证了实现的系统的正确性。实现了UML建模过程和转换后的模型的自动化验证过程的集成。