使用π-演算验证两阶段提交协议  

The Two Phase Commit Protocol in π-Calculus

作　　者：张帆[1] 李舟军[2] 孙云[1] 

机构地区：[1]国防科技大学计算机学院,长沙410073 [2]北京航空航天大学计算机学院,北京100083

出　　处：《计算机科学》2006年第11期268-271,共4页Computer Science

基　　金：国家自然科学基金项目(90104026;60473057)

摘　　要：两阶段提交协议是最简单且最常用的原子提交协议,该协议使分布式事务的提交具有原子性和持久性。在本文中,我们使用π-演算对两阶段提交协议进行描述,并对其正确性进行了证明,进一步体现了π-演算对于描述进程通信及并行性的独特优势。The two phase commit protocol is the simplest and most popular atomic commitment protocol （ACP）. It makes the transaction commitment in the distributed systems have atomicity and durability. In this paper, we use the π-calculus to describe the two phase commit protocol, and prove the correctness, and also incarnate, the unique predominance of π-calculus in description of process communication and parallelism.

关 键 词：两阶段提交协议 形式化 异步π演算 互模拟 

分 类 号：TP311.133[自动化与计算机技术—计算机软件与理论]