中文摘要：

语义业务流程管理（SBPM）是一个崭新的研究领域，它对于提高业务流程的自动化水平有着重要的理论意义及应用前景。本项目以语义Web的本体表示、推理技术和Petri网形式化方法为手段，研究语义业务流程模型验证的基础理论及方法体系，为语义业务流程模型验证的规范化、完备化打下理论基础。首先，建立语义业务流程模型的业务约束规则体系及其基于语义Web规则语言的逻辑表示；其次，结合语义业务流程模型本体，使用推理机验证模型的模式正确性和业务一致性；另外，研究语义业务流程模型到本体Petri网形式化模型的双向映射，通过Petri网工具验证语义业务流程模型的语义一致性。通过上述研究，本项目将建立具有坚实理论基础的、具备通用性和完备性的对语义业务流程模型进行自动分析与验证的理论、技术体系，为语义业务流程模型验证的进一步研究与应用提供新思路和理论依据。

结论摘要：

语义业务流程建模是一个新兴的研究领域，它与传统的业务流程管理相比实现了业务流程的机器可读、可理解，提高了流程的自动化处理程度。语义业务流程模型（SBPM）是实现语义业务流程管理的基础，模型的正确性又是SBPM成功实施的前提和关键。因此，语义业务流程建模及模型的正确性验证对于促进语义业务流程管理的应用有着重要的意义。我们针对这些问题进行了深入研究。首先，建立了三个初始实验模型，分析了（1）基于BPMN本体（BPMNO）和领域本体（DO）构建语义业务流程、（2）在业务流程建模本体（BPMO）基础上对业务流程建模，通过这两种语义业务流程建模方式来研究业务流程的需求规则与模式规则，包括连接规则、匹配规则（合并公理）、内部具体规则。为了完成对流程模型的正确性验证，我们设计了验证环节，通过SWRL对业务规则的形式化描述，使用M-propagation和I-propagation算法进行验证，确保流程的一致性和完整性，保证流程的正确执行。其次，我们研究了基于Pi演算的业务流程形式化模型映射、交互与验证，分析了服务交互的基本特征，然后给出基于Pi演算的交互行为的形式化表达方式；最后以Web服务为例进行了较详尽的建模，并进行了推演验证。同时，为解决可验证需求语义特征的建模方法与工具支持，研究并提出一种BPR框架下可出具验证的可视化建模工具。该工具在具备基本的可视化业务流程建模功能基础上，可通过与随机Petri网性能计算工具协同计算，从可覆盖性等角度验证流程属性满足需求语义的合法性。