随着跨组织流程在企业信息系统领域的快速发展,组织间流程的交互、多个流程的编排等逐渐取代组织内的工作流而成为流程建模人员关注的焦点和工作的中心。而传统的建模方法又不能适应这种跨组织业务流程的建模需求,所以进行跨组织业务流程建模的研究具有重要的现实意义。本文以云计算环境下跨组织业务流程建模作为研究课题,对跨组织流程的特点和云计算环境下的业务流程特征进行深入分析；对业务流程从组织间的流程柔性、流程交互以及流程编排等三个方面进行了形式化建模方法研究。本文所做的主要工作如下：(1)柔性业务流程建模的研究。分析了柔性业务流程的特点,将柔性业务流程划分为动态选择型、变更型和异常型三类。提出了将业务流程图中的BPMN元素映射到基于π演算的形式化模型的映射规则。针对上述三种类型的柔性流程的结构,应用π演算语法给出了相应的描述形式。最后通过具体流程实例进行了实例建模,并应用MWB验证工具对模型进行了推演验证,验证了模型的正确性。(2)服务交互建模的研究。针对基本的服务交互方式,应用π演算的通道移动性特点给出了服务交互的表达方法。同时,将全部13个服务交互模式进行了完整的形式化建模。文中给出了Web服务模型和云服务交互模型的建模实例,并进行了推演验证。结果表明服务交互中的动态、开放的特性能够用π演算语法给予充分地表达。(3)编排建模的研究。分析了标准BPMN在编排建模方面的不足,探讨了基于BPMN2.0Choreography的编排建模方法,并给出了一个网上购物支付流程的编排图实例。定义了一个从编排的活动集合到π演算语义表达式的函数,并通过该函数给出了BPMN2.0Choreography元素映射到π演算语法的一组定义,分别对编排的基本活动和结构化动作进行建模定义,从而建立基于π演算的编排建模的形式化方法。最后给出拍卖流程的建模实例,并针对拍卖流程的编排模型进行了模拟推演验证。(4)跨组织流程统一建模方法应用研究。研究对跨组织业务流程统一进行编制与编排建模的方法。提出了将业务流程从编排开始建模,至顶向下,逐步细化。按照“编排图—交互图—协作图—流程图”的顺序逐步映射转换。以拍卖场景业务流程作为实例,对跨组织业务流程的建模方法系统地进行了全面的应用。本文的创新点主要包括以下几个部分：(1)应用π演算的通道移动性给出了服务交互的表达方法,实现了对并发进程复杂通道的简洁灵活的描述。通过扩展π演算语法,进一步丰富了π演算的表达能力,克服了现有方法不能有效地表示异常中断和超时处理行为的缺陷,实现了对异常型业务流程的有效表示,满足了柔性流程三种类型的形式化建模需求,推进了柔性业务流程建模方法的发展。(2)基于π演算理论对业务流程编排进行建模,真正从全局视角形式化建模跨组织业务流程,改变了以往过早关注流程细节和交互细节的倾向。(3)提出了跨组织流程统一建模方法,完成了编排活动至编制活动的有效转换。该建模方法同时使用图形描述与形式化表达,从而在保持业务流程模型的可读性的同时又实现了模型的严谨性,便于分析和验证。实例表明所构建的模型结构清晰、层次分明、描述简练,显示出该建模方法具有对构建跨组织业务流程模型的超强的表达能力。本研究成果对于在云计算环境下的业务流程形式化建模方法的发展具有较高的学术意义和较大的应用价值。