随着信息技术的快速发展，计算机应用日益广泛，软件已渗透到国民经济和国防建设的各个领域。但是软件的生产现状和质量常常存在缺陷。因此，如何提高软件的质量，尤其在一些安全关键应用领域，保证软件的可靠性和安全性已成为国内外研究的热点问题。软件的可靠性不仅取决于软件开发的方法和过程，也取决于软件的测试和验证。统一建模语言UML已广泛应用于安全关键计算机系统的开发中。它是一种功能强大、面向对象的可视化系统分析建模语言。但UML是半形式化的，不能用数学工具直接的表达和分析，而且对象之间约束规则的一致性和并发性很难被UML模型所描述，其系统的动态行为特征也难于全面地用UML模型体现。Petri网是一种系统的数学和图形的建模分析工具，它以图形化的数学工具库所、变迁来清楚地描述系统内部的相互作用，它特别适合描述系统中进程或者部件的顺序、并发、冲突以及同步等关系。因此，本文提出了一种将“UML状态图模型转换为Petri网模型的方法”，并基于该方法，初步实现了一个将UML状态图模型转换为Petri网模型的自动转换工具。论文主要工作包括以下几点：　　 (1)针对国内外的研究现状，对软件系统的形式化建模、描述及验证方法的研究和应用进行了分析。　　 (2)对UML状态图进行了研究，给出了UML状态图的形式化定义，并用定义的形式化语言描述了状态图的相关性质、基本状态和复合状态。　　 (3)通过分析UML状态图的形式化定义和Petri网严格的形式化语义，研究了两者语义之间的等价部分，提出了将UML状态图转换为Petri网的方法。　　 (4)基于UML状态图的形式化定义、Petri网的形式化语义以及XML文档的结构，本文提出了UML状态图到Petri网的转换方法，实现了一个将“UML状态图模型转换为Petri网模型”的自动转换工具。　　 (5)以一种新型的分散式铁路联锁系统(DRIS)为例，对本文实现的自动转换工具进行了检验。