摘要：补偿通信顺序进程（cCSP）是通信顺序进程用于长事务建模的扩展，可用来描述服务计算中的编制程序，比如WS-BPEL程序。目前，cCSP只有操作语义和基于迹的指称语义，对死锁和发散行为的推理支持不够。本文扩展了cCSP，引入新的组合操作子，给出扩展cCSP的失败发散语义；并根据该语义，给出新引入组合操作子的重要代数规则，用于语义的理解和佐证。最后，给出一个案例描述用于展示扩展cCSP。

关键词：补偿通信顺序进程 指称语义 失败发散语义 代数规则 

单位：国防科学技术大学计算机学院 湖南长沙410073