补偿通信顺序进程的扩展及失败发散语义

摘要

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