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

doi:10.3969/j.issn.1007130X.2010.

J4 ›› 2010, Vol. 32 ›› Issue (3): 89-95.doi: 10.3969/j.issn.1007130X.2010.

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

陈振邦, 王戟, 齐治昌

（国防科学技术大学计算机学院，湖南长沙 410073）

收稿日期:2009-01-06 修回日期:2009-03-12 出版日期:2010-03-10 发布日期:2010-03-10
通讯作者: 陈振邦 E-mail:zbchen@nudt.edu.cn
作者简介:陈振邦(1981)，男，湖北黄陂人，博士生，研究方向为软件体系结构、面向服务的软件工程和软件验证；王戟，博士，教授，博士生导师，研究方向为形式化方法、高可信软件工程；齐治昌，教授，博士生导师，研究方向为软件工程。

An Extended cCSP with Failure Divergence Semantics

CHEN Zhen-Bang, WANG Ji, JI Chi-Chang

(School of Computer Science,National University of Defense Technology,Changsha 410073,China)

Received:2009-01-06 Revised:2009-03-12 Online:2010-03-10 Published:2010-03-10
Contact: CHEN Zhen-Bang E-mail:zbchen@nudt.edu.cn

摘要/Abstract

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

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

Abstract: 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.

Key words: ompensating CSP;denotational semantics;failuredivergence semantics;algebraic law

中图分类号:

TP311

陈振邦, 王戟, 齐治昌. 补偿通信顺序进程的扩展及失败发散语义[J]. J4, 2010, 32(3): 89-95.

CHEN Zhen-Bang, WANG Ji, JI Chi-Chang. An Extended cCSP with Failure Divergence Semantics[J]. J4, 2010, 32(3): 89-95.

[1]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[2]	刘璘1,毛新军2. Agent、目标与情景结合的需求方法[J]. J4, 2010, 32(6): 1-8.
[3]	武凌,马季. 基于状态信息的分散式工作流管理系统模型的研究[J]. J4, 2010, 32(6): 40-44.
[4]	马淑娇，叶春明，杨坚争. Mobile Agent在分布式数据库信息查询的应用研究[J]. J4, 2010, 32(6): 103-105.
[5]	袁文杰，应时，吴可嘉，姚俊峰. 基于π演算的反射式需求规约描述方法[J]. J4, 2010, 32(6): 146-149.
[6]	赵楷1,2，应时1，胡罗凯1，曾志浩1，袁文杰1. 一种基于Agent的语义Web服务编制框架[J]. J4, 2010, 32(6): 150-154.
[7]	曹春,马晓星,陶先平. ArtemisCOOR:一个基于Agent的软件动态协同支撑平台[J]. J4, 2010, 32(5): 1-5.
[8]	李克文，张自鲁. 基于遗传-蚁群混合算法的软件测试数据自动生成方法[J]. J4, 2010, 32(5): 51-53.
[9]	李童，刘璘. 一种面向主体的服务规则模拟验证方法[J]. J4, 2010, 32(5): 67-73.
[10]	赖如洁1，曹健1，李明禄1，赵海燕2. 服务Agent的设计与实现[J]. J4, 2010, 32(5): 113-117.
[11]	王春红1,任姚鹏1，徐学洲2. 基于等级策略的构件聚类研究[J]. J4, 2010, 32(5): 118-120.
[12]	张辉1，张珍2. 一种基于多映射的分布式本体融合框架[J]. J4, 2010, 32(5): 130-132.
[13]	黄谷,缪力,张大方. 802.11i双向认证协议的模型检查[J]. J4, 2010, 32(4): 25-28.
[14]	曾一，王健，洪媛，周欣，蔡森虎. 一种支持MDA的UML类图到RDB模型的转换方法[J]. J4, 2010, 32(4): 67-70.
[15]	李卓，邓明荣. 相似代码检测工具及其案例分析[J]. J4, 2010, 32(4): 71-74.

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

An Extended cCSP with Failure Divergence Semantics

PDF

可视化

摘要/Abstract

引用本文

使用本文

相关文章 15

编辑推荐

Metrics

本文评价