随着世界经济和技术蓬勃发展,业务流程管理在科研领域和企业运用领域都有着很高的关注度。国内外专家学者们探索着流程管理的思想和方法,与此同时,企业也在科研成果的基础上,通过业务流程的优化和改善提高企业竞争力和扩大市场占有率。面向主语的业务流程管理(S-BPM)是业务流程管理领域最新提出的一种思想,符合自然语言的标准语序自然语言结构主语-谓语-宾语,它使得业务流程和自然语言的语序一样更容易被人们所理解；其结构清晰,对于科研和运用都表现出了很好的价值。W.M.P.van der Aalst等专家总结了业务流程建模过程当中经常出现的工作流模式,用来比较不同建模工具的适用性和有效性,提供了一个评估的有效标准。PI演算作为一种描述移动系统的进程代数,可用于对并发和动态变化的系统进行建模,在并发和分布式理论研究中处于非常重要的地位。本文针对新兴业务流程比传统业务流程的复杂性和多变性,分析传统建模方法的局限性,引入S-BPM的业务流程管理思想；首先,讨论了S-BPM下PASS建模方法的局限性和不完备性,定义相对规范S-BPM建模方法PASS++,并对PASS++的表达能力进行了分析和验证,同时对比评估了PASS++的建模能力；然后,对PASS++下PI演算形式化理论基础进行了分析,提出PASS++到PI演算的映射,并提出了PASS++定制工具的基本结构；最后,提出运用形式化验证工具MWB,对业务流程模型进行仿真和验证。期望本文所做工作对构建基于S-BPM的业务流程分析、建模、仿真、验证的架构体系有一定的研究价值和实践指导意义。本文的主要创新特点是：I、分析S-BPM的PASS建模方法的局限性和不完备性,定义相对规范S-BPM建模方法PASS++,并对PASS++的表达能力进行了分析和验证；II、比较分析PASS++的建模能力,并提出PASS++定制工具的基本结构；III、对PASS++下PI演算形式化理论基础进行了分析,提出PASS++和PI演算的映射规则。