工作流技术是实现企业业务过程建模、过程管理与过程自动化的核心技术。随着信息技术的发展和计算机应用的普及，工作流技术正在受到越来越多的关注。在与工作流相关的各类技术中，工作流建模技术是当前研究的一个热点。 在工作流技术的几个研究方向中，工作流模型和工作流模型的验证既是工作流技术研究的基础，也是工作流领域的重点研究方向。 形式化模型验证技术是验证有穷状态的并发系统正确性的一种方法.在形式化模型检测中，系统的正确性被描述成时序逻辑的一个断言，并且存在成熟的算法去高效的检测这个断言成立或者不成立.形式化模型检测技术在协议验证中起着广泛的作用。 本文结合国家高技术产业化示范工程项目“青鸟电子政务支撑平台”和国家自然科学基金项目“基于Petri网的工作流系统构造技术和模型验证方法”，结合PNML描述语言，对基于PETRI网的工作流模型语义层的验证给出了详细的描述.本文主要贡献有以下几点，第一是给出了工作流语义层正确性的定义，第二描述了如何把形式化模型验证技术运用在基于Petri网的工作流模型的语义层的验证上，给出了从Petri网描述的工作流模型转换到可以被形式化验证的自动机模型的基本算法，第三描述了整个系统的实现。 论文第一章简要介绍了工作流系统的基本概念及论文的工作背景；第二章系统地说明了基于Petri网的层次化工作流模型和模型定义语言；第三章具体论述形式化模型验证技术的基本理论，算法，和支持工具；第四章描述了语义层的验证算法，并给出了实例和系统实现。最后第五章总结了论文的成果，并对进一步的工作提出了设想。