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