北京大学学报（自然科学版）

• 北京大学学报 •

基于时序可中断π演算的BPEL和BPEL4People建模

金?,王捍贫,朱梅霞   

  1. 北京大学信息科学技术学院, 北京 100871;
  • 收稿日期:2011-04-06 出版日期:2012-03-20 发布日期:2012-03-20

Modeling BPEL and BPEL4People with a Timed Interruptable ?-Calculus

JIN Wei, WANG Hanpin, ZHU Meixia   

  1. School of Electronics Engineering and Computer Science, Peking University, Beijing 100871;
  • Received:2011-04-06 Online:2012-03-20 Published:2012-03-20

PDF

PDF (翻译版)

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

关键词: BPEL, BPEL4People, π演算, 时序, 可中断

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

Key words: BPEL, BPEL4People, π-calculus, timing, interruptable

中图分类号: 

版权所有 © 《北京大学学报（自然科学版）》编辑部
技术支持：北京玛格泰克科技发展有限公司