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

An Extended cCSP with Failure Divergence Semantics

作　　者：陈振邦[1] 王戟[1] 齐治昌[1] 

机构地区：[1]国防科学技术大学计算机学院

出　　处：《计算机工程与科学》2010年第3期89-95,110,共8页Computer Engineering & Science

基　　金：国家973计划资助项目(2005CB321802);自然科学基金资助项目(90612009;60803042)

摘　　要：补偿通信顺序进程(cCSP)是通信顺序进程用于长事务建模的扩展,可用来描述服务计算中的编制程序,比如WS-BPEL程序。目前,cCSP只有操作语义和基于迹的指称语义,对死锁和发散行为的推理支持不够。本文扩展了cCSP,引入新的组合操作子,给出扩展cCSP的失败发散语义;并根据该语义,给出新引入组合操作子的重要代数规则,用于语义的理解和佐证。最后,给出一个案例描述用于展示扩展cCSP。Compensating CSP （cCSP） is an extension to CSP for modeling long-running transactions. It can be used to specify the programs written in orchestration languages, such as WS-BPEL. cCSP has only an operational semantics and a trace semantics that are not expressive enough for reasoning about deadlock and divergence. We extend cCSP with more operators and define for it a failure-divergence semantics. The significant algebraic laws are presented for the new operators with respect to the new semantics for its justification as well as for understanding. In addition, a case study is given to demonstrate the extended cCSP.

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

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