论文部分内容阅读
根据WS—Business Activity规范提出一个扩展的长事务协议BAPC，该协议较为详细和更接近于软件实现。BAPC协议放松了传统事务中的ACID属性的限制，重新定义了松耦合环境下事务性质。因此在BAPC协议的软件实施中，迫切需要对BAPC协议进行形式化分析，以保证协议的正确性。基于简洁的异步PI演算，建模和分析了BAPC协议，采用互模拟等价理论及迁移语义给出了BAPC协议的满足长事务协议所具有的持久性、可终止性和局部原子性的证明，说明该协议可以用于处理基本Web服务组合事务，能够保证组合服务的长