中文摘要：

业务过程管理技术(BPM)和面向服务体系结构(SOA)的出现，使得基于服务的协同业务过程成为企业间协作的重要手段。本课题以π演算为基础，对协同业务过程形式化建模和分析中的关键技术进行研究。首先对π演算进行扩展，提出一种Cπ演算，用于对协同业务过程进行建模。在此基础上进行下述分析，以保证协同业务过程的正确性、一致性和安全性。(1)协同模式分析总结出协同业务过程中的协同模式，并用规约的方法证明协同模式的正确性。(2)一致性分析通过部分互模拟语义定义出进程的一致性度量，用以分析协同业务过程与全局业务过程的一致性，以保证协同业务过程能够满足企业的业务目标。(3)安全性分析建立支持多态和子类型的类型系统，用类型分析的方法来保证协同业务过程能够满足企业的访问控制安全策略。最后，开发出一个协同业务过程建模和分析工具。本课题的研究工作将对协同业务过程管理系统的开发和验证提供理论指导与工程方法。

结论摘要：

业务过程管理技术(BPM)和面向服务体系结构(SOA)的出现，使得基于服务的协同业务过程成为企业间协作的重要手段。本课题以π演算为基础，对协同业务过程形式化建模和分析中的关键技术进行研究。研究内容包括: (1)协同模式分析。总结出了协同业务过程中的7种基本模式和45种协同模式。(2)正确性分析。提出了基于π演算进行企业业务过程交互行为建模以及协同业务过程正确性分析的方法。(3)一致性分析。提出了一种基于互模拟博弈图的进程一致性度量方法，用以分析协同业务过程与全局业务过程的一致性。(4)安全性分析。通过分析协同业务过程中的业务需求，提出了一种主动授权模型及其约束分析方法，提出了混合系统的不变量分析方法。在研究成果方面，共发表论文13篇，其中2篇SCI，10篇EI。在人才培养方面，培养3名硕士生顺利毕业。本课题的研究基本完成预定计划。本课题的研究工作将对协同业务过程管理系统的开发和验证提供理论指导与工程方法。