位置:成果数据库 > 期刊 > 期刊详情页
基于时序可中断π演算的BPEL和BPEL4People建模
  • ISSN号:0479-8023
  • 期刊名称:北京大学学报(自然科学版)
  • 时间:2012
  • 页码:209-216
  • 分类:TP301[自动化与计算机技术—计算机系统结构;自动化与计算机技术—计算机科学与技术]
  • 作者机构:[1]北京大学信息科学技术学院,北京100871
  • 相关基金:国家自然科学基金(760873061,60821003,61033006)和国家重点基础研究发展计划(2009cB320701,2010CB328103)资助
  • 相关项目:基于分离逻辑的程序验证方法研究
中文摘要:

为了形式化地定义BPEL和BPEL4People的语义,提出了一个π演算的变种——πit演算。相对于传统的π演算,πit演算可以描述中断事件和时间事件,从而拥有更好的建模表达能力。介绍了7ci。演算的语法和语义,定义了一类强互模拟关系来判定πit算进程间的行为等价,然后使用πit。演算对BPEL和BPEL4People的活动进行了建模。该形式化模型有助于在BPEL和BPEL4People程序的设计阶段对其可靠性和一致性进行验证。

英文摘要:

To describe formal semantics of business processing execution language (BPEL) and BPEL for people (BPEL4People), the authors introduce the πit-calculus, a new variant of the π-calculus. The execution of nit-calculus can be interrupted and can handle timing events as well. Both syntax and semantics of the πit-calculus are provided. A strong bisimulation relation that specifies when two processes can be considered as the same is also given. The activities of BPEL and BPEL4People are modeled by the new calculus. The formal framework may facilitate the reliability and consistency analysis in BPEL or BPEL4People design process

同期刊论文项目
期刊论文 42 会议论文 43
期刊论文 36 会议论文 54 获奖 2
同项目期刊论文
期刊信息
  • 《北京大学学报:自然科学版》
  • 中国科技核心期刊
  • 主管单位:教育部
  • 主办单位:北京大学
  • 主编:赵光达
  • 地址:北京海淀区海淀路52号
  • 邮编:100871
  • 邮箱:xbna@pku.edu.cn
  • 电话:010-62756706
  • 国际标准刊号:ISSN:0479-8023
  • 国内统一刊号:ISSN:11-2442/N
  • 邮发代号:2-89
  • 获奖情况:
  • 1997年第二届全国优秀科技期刊评比一等奖,1999年教育部“优秀自然科学学报一等奖”,1999年获首届国家期刊奖,中国期刊方阵“双高”期刊
  • 国内外数据库收录:
  • 俄罗斯文摘杂志,美国化学文摘(网络版),美国数学评论(网络版),德国数学文摘,荷兰文摘与引文数据库,英国科学文摘数据库,英国动物学记录,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊(2004版),中国北大核心期刊(2008版),中国北大核心期刊(2011版),中国北大核心期刊(2014版),英国英国皇家化学学会文摘,中国北大核心期刊(2000版)
  • 被引量:18270