|
|||||
|
|
| 基于时序可中断π演算的BPEL和BPEL4People建模 | |
| 作者姓名： | 金暐 王捍贫 朱梅霞 |
| 作者单位： | 北京大学信息科学技术学院 |
| 基金项目： | 国家自然科学基金(760873061,60821003,61033006);国家重点基础研究发展计划(2009CB320701,2010CB328103)资助 |
| 摘 要： | 为了形式化地定义BPEL和BPEL4People的语义,提出了一个π演算的变种——πit演算。相对于传统的π演算,πit演算可以描述中断事件和时间事件,从而拥有更好的建模表达能力。介绍了πit演算的语法和语义,定义了一类强互模拟关系来判定πit演算进程间的行为等价,然后使用πit演算对BPEL和BPEL4People的活动进行了建模。该形式化模型有助于在BPEL和BPEL4People程序的设计阶段对其可靠性和一致性进行验证。 |
| 关 键 词： | BPEL BPELPeople π演算 时序 可中断 |
| 本文献已被 CNKI 等数据库收录！ | |